Theorem mhlem1 877

Description: Lemma for Marsden-Herman distributive law. (Contributed by NM, 10-Mar-2002.)

Hypotheses

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

Assertion

Ref	Expression
mhlem1	((a ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ c))

Proof of Theorem mhlem1

Step	Hyp	Ref	Expression
1		df-t 41	. . . . 5 1 = (b ∪ b⊥ )
2	1	lan 77	. . . 4 ((a ∪ b) ∩ 1) = ((a ∪ b) ∩ (b ∪ b⊥ ))
3		an1 106	. . . 4 ((a ∪ b) ∩ 1) = (a ∪ b)
4		comor2 462	. . . . . 6 (a ∪ b) C b
5	4	comcom2 183	. . . . . 6 (a ∪ b) C b⊥
6	4, 5	fh1 469	. . . . 5 ((a ∪ b) ∩ (b ∪ b⊥ )) = (((a ∪ b) ∩ b) ∪ ((a ∪ b) ∩ b⊥ ))
7		ax-a2 31	. . . . 5 (((a ∪ b) ∩ b) ∪ ((a ∪ b) ∩ b⊥ )) = (((a ∪ b) ∩ b⊥ ) ∪ ((a ∪ b) ∩ b))
8		mhlem1.1	. . . . . . . . . 10 a C b
9	8	comcom2 183	. . . . . . . . 9 a C b⊥
10	9	comcom 453	. . . . . . . 8 b⊥ C a
11		comid 187	. . . . . . . . 9 b C b
12	11	comcom3 454	. . . . . . . 8 b⊥ C b
13	10, 12	fh1r 473	. . . . . . 7 ((a ∪ b) ∩ b⊥ ) = ((a ∩ b⊥ ) ∪ (b ∩ b⊥ ))
14		dff 101	. . . . . . . . 9 0 = (b ∩ b⊥ )
15	14	lor 70	. . . . . . . 8 ((a ∩ b⊥ ) ∪ 0) = ((a ∩ b⊥ ) ∪ (b ∩ b⊥ ))
16	15	ax-r1 35	. . . . . . 7 ((a ∩ b⊥ ) ∪ (b ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ 0)
17		or0 102	. . . . . . 7 ((a ∩ b⊥ ) ∪ 0) = (a ∩ b⊥ )
18	13, 16, 17	3tr 65	. . . . . 6 ((a ∪ b) ∩ b⊥ ) = (a ∩ b⊥ )
19		ancom 74	. . . . . . 7 ((a ∪ b) ∩ b) = (b ∩ (a ∪ b))
20		ax-a2 31	. . . . . . . 8 (a ∪ b) = (b ∪ a)
21	20	lan 77	. . . . . . 7 (b ∩ (a ∪ b)) = (b ∩ (b ∪ a))
22		anabs 121	. . . . . . 7 (b ∩ (b ∪ a)) = b
23	19, 21, 22	3tr 65	. . . . . 6 ((a ∪ b) ∩ b) = b
24	18, 23	2or 72	. . . . 5 (((a ∪ b) ∩ b⊥ ) ∪ ((a ∪ b) ∩ b)) = ((a ∩ b⊥ ) ∪ b)
25	6, 7, 24	3tr 65	. . . 4 ((a ∪ b) ∩ (b ∪ b⊥ )) = ((a ∩ b⊥ ) ∪ b)
26	2, 3, 25	3tr2 64	. . 3 (a ∪ b) = ((a ∩ b⊥ ) ∪ b)
27	26	ran 78	. 2 ((a ∪ b) ∩ (b⊥ ∪ c)) = (((a ∩ b⊥ ) ∪ b) ∩ (b⊥ ∪ c))
28		comorr 184	. . . . 5 b⊥ C (b⊥ ∪ c)
29	28	comcom6 459	. . . 4 b C (b⊥ ∪ c)
30		comanr2 465	. . . . 5 b⊥ C (a ∩ b⊥ )
31	30	comcom6 459	. . . 4 b C (a ∩ b⊥ )
32	29, 31	fh2rc 480	. . 3 (((a ∩ b⊥ ) ∪ b) ∩ (b⊥ ∪ c)) = (((a ∩ b⊥ ) ∩ (b⊥ ∪ c)) ∪ (b ∩ (b⊥ ∪ c)))
33		leao2 163	. . . . 5 (a ∩ b⊥ ) ≤ (b⊥ ∪ c)
34	33	df2le2 136	. . . 4 ((a ∩ b⊥ ) ∩ (b⊥ ∪ c)) = (a ∩ b⊥ )
35	34	ax-r5 38	. . 3 (((a ∩ b⊥ ) ∩ (b⊥ ∪ c)) ∪ (b ∩ (b⊥ ∪ c))) = ((a ∩ b⊥ ) ∪ (b ∩ (b⊥ ∪ c)))
36	32, 35	ax-r2 36	. 2 (((a ∩ b⊥ ) ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ (b⊥ ∪ c)))
37	11	comcom2 183	. . . . 5 b C b⊥
38		mhlem1.2	. . . . . 6 c C b
39	38	comcom 453	. . . . 5 b C c
40	37, 39	fh1 469	. . . 4 (b ∩ (b⊥ ∪ c)) = ((b ∩ b⊥ ) ∪ (b ∩ c))
41	14	ax-r5 38	. . . . 5 (0 ∪ (b ∩ c)) = ((b ∩ b⊥ ) ∪ (b ∩ c))
42	41	ax-r1 35	. . . 4 ((b ∩ b⊥ ) ∪ (b ∩ c)) = (0 ∪ (b ∩ c))
43		or0r 103	. . . 4 (0 ∪ (b ∩ c)) = (b ∩ c)
44	40, 42, 43	3tr 65	. . 3 (b ∩ (b⊥ ∪ c)) = (b ∩ c)
45	44	lor 70	. 2 ((a ∩ b⊥ ) ∪ (b ∩ (b⊥ ∪ c))) = ((a ∩ b⊥ ) ∪ (b ∩ c))
46	27, 36, 45	3tr 65	1 ((a ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ c))

This proof depends on syntax axioms:   = wb 1   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  mhlem2  878