Theorem mhlem1 859

Description: Lemma for Marsden-Herman distributive law.

Hypotheses

Ref	Expression
mhlem1.1	a C b
mhlem1.2	c C b

Assertion

Ref	Expression
mhlem1	((a v b) ^ (b_|_ v c)) = ((a ^ b_|_) v (b ^ c))

Proof of Theorem mhlem1

Step	Hyp	Ref	Expression
1		df-t 40	. . . . 5 1 = (b v b_|_)
2	1	lan 70	. . . 4 ((a v b) ^ 1) = ((a v b) ^ (b v b_|_))
3		an1 98	. . . 4 ((a v b) ^ 1) = (a v b)
4		comor2 444	. . . . . 6 (a v b) C b
5	4	comcom2 175	. . . . . 6 (a v b) C b_|_
6	4, 5	fh1 451	. . . . 5 ((a v b) ^ (b v b_|_)) = (((a v b) ^ b) v ((a v b) ^ b_|_))
7		ax-a2 30	. . . . 5 (((a v b) ^ b) v ((a v b) ^ b_|_)) = (((a v b) ^ b_|_) v ((a v b) ^ b))
8		mhlem1.1	. . . . . . . . . 10 a C b
9	8	comcom2 175	. . . . . . . . 9 a C b_|_
10	9	comcom 435	. . . . . . . 8 b_|_ C a
11		comid 179	. . . . . . . . 9 b C b
12	11	comcom3 436	. . . . . . . 8 b_|_ C b
13	10, 12	fh1r 455	. . . . . . 7 ((a v b) ^ b_|_) = ((a ^ b_|_) v (b ^ b_|_))
14		dff 93	. . . . . . . . 9 0 = (b ^ b_|_)
15	14	lor 66	. . . . . . . 8 ((a ^ b_|_) v 0) = ((a ^ b_|_) v (b ^ b_|_))
16	15	ax-r1 34	. . . . . . 7 ((a ^ b_|_) v (b ^ b_|_)) = ((a ^ b_|_) v 0)
17		or0 94	. . . . . . 7 ((a ^ b_|_) v 0) = (a ^ b_|_)
18	13, 16, 17	3tr 62	. . . . . 6 ((a v b) ^ b_|_) = (a ^ b_|_)
19		ancom 68	. . . . . . 7 ((a v b) ^ b) = (b ^ (a v b))
20		ax-a2 30	. . . . . . . 8 (a v b) = (b v a)
21	20	lan 70	. . . . . . 7 (b ^ (a v b)) = (b ^ (b v a))
22		a5c 113	. . . . . . 7 (b ^ (b v a)) = b
23	19, 21, 22	3tr 62	. . . . . 6 ((a v b) ^ b) = b
24	18, 23	2or 67	. . . . 5 (((a v b) ^ b_|_) v ((a v b) ^ b)) = ((a ^ b_|_) v b)
25	6, 7, 24	3tr 62	. . . 4 ((a v b) ^ (b v b_|_)) = ((a ^ b_|_) v b)
26	2, 3, 25	3tr2 61	. . 3 (a v b) = ((a ^ b_|_) v b)
27	26	ran 71	. 2 ((a v b) ^ (b_|_ v c)) = (((a ^ b_|_) v b) ^ (b_|_ v c))
28		comorr 176	. . . . 5 b_|_ C (b_|_ v c)
29	28	comcom6 441	. . . 4 b C (b_|_ v c)
30		comanr2 447	. . . . 5 b_|_ C (a ^ b_|_)
31	30	comcom6 441	. . . 4 b C (a ^ b_|_)
32	29, 31	fh2rc 462	. . 3 (((a ^ b_|_) v b) ^ (b_|_ v c)) = (((a ^ b_|_) ^ (b_|_ v c)) v (b ^ (b_|_ v c)))
33		leao2 155	. . . . 5 (a ^ b_|_) =< (b_|_ v c)
34	33	df2le2 128	. . . 4 ((a ^ b_|_) ^ (b_|_ v c)) = (a ^ b_|_)
35	34	ax-r5 37	. . 3 (((a ^ b_|_) ^ (b_|_ v c)) v (b ^ (b_|_ v c))) = ((a ^ b_|_) v (b ^ (b_|_ v c)))
36	32, 35	ax-r2 35	. 2 (((a ^ b_|_) v b) ^ (b_|_ v c)) = ((a ^ b_|_) v (b ^ (b_|_ v c)))
37	11	comcom2 175	. . . . 5 b C b_|_
38		mhlem1.2	. . . . . 6 c C b
39	38	comcom 435	. . . . 5 b C c
40	37, 39	fh1 451	. . . 4 (b ^ (b_|_ v c)) = ((b ^ b_|_) v (b ^ c))
41	14	ax-r5 37	. . . . 5 (0 v (b ^ c)) = ((b ^ b_|_) v (b ^ c))
42	41	ax-r1 34	. . . 4 ((b ^ b_|_) v (b ^ c)) = (0 v (b ^ c))
43		or0r 95	. . . 4 (0 v (b ^ c)) = (b ^ c)
44	40, 42, 43	3tr 62	. . 3 (b ^ (b_|_ v c)) = (b ^ c)
45	44	lor 66	. 2 ((a ^ b_|_) v (b ^ (b_|_ v c))) = ((a ^ b_|_) v (b ^ c))
46	27, 36, 45	3tr 62	1 ((a v b) ^ (b_|_ v c)) = ((a ^ b_|_) v (b ^ c))

Syntax hints:   = wb 1   C wc 3  _|_wn 4   v wo 6   ^ wa 7  1wt 9  0wf 10

This theorem is referenced by:  mhlem2 860

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org