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 ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ c))

Proof of Theorem mhlem1

Step	Hyp	Ref	Expression
1		df-t 40	. . . . 5 1 = (b ∪ b⊥ )
2	1	lan 70	. . . 4 ((a ∪ b) ∩ 1) = ((a ∪ b) ∩ (b ∪ b⊥ ))
3		an1 98	. . . 4 ((a ∪ b) ∩ 1) = (a ∪ b)
4		comor2 444	. . . . . 6 (a ∪ b) C b
5	4	comcom2 175	. . . . . 6 (a ∪ b) C b⊥
6	4, 5	fh1 451	. . . . 5 ((a ∪ b) ∩ (b ∪ b⊥ )) = (((a ∪ b) ∩ b) ∪ ((a ∪ b) ∩ b⊥ ))
7		ax-a2 30	. . . . 5 (((a ∪ b) ∩ b) ∪ ((a ∪ b) ∩ b⊥ )) = (((a ∪ b) ∩ b⊥ ) ∪ ((a ∪ 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 ∪ b) ∩ b⊥ ) = ((a ∩ b⊥ ) ∪ (b ∩ b⊥ ))
14		dff 93	. . . . . . . . 9 0 = (b ∩ b⊥ )
15	14	lor 66	. . . . . . . 8 ((a ∩ b⊥ ) ∪ 0) = ((a ∩ b⊥ ) ∪ (b ∩ b⊥ ))
16	15	ax-r1 34	. . . . . . 7 ((a ∩ b⊥ ) ∪ (b ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ 0)
17		or0 94	. . . . . . 7 ((a ∩ b⊥ ) ∪ 0) = (a ∩ b⊥ )
18	13, 16, 17	3tr 62	. . . . . 6 ((a ∪ b) ∩ b⊥ ) = (a ∩ b⊥ )
19		ancom 68	. . . . . . 7 ((a ∪ b) ∩ b) = (b ∩ (a ∪ b))
20		ax-a2 30	. . . . . . . 8 (a ∪ b) = (b ∪ a)
21	20	lan 70	. . . . . . 7 (b ∩ (a ∪ b)) = (b ∩ (b ∪ a))
22		a5c 113	. . . . . . 7 (b ∩ (b ∪ a)) = b
23	19, 21, 22	3tr 62	. . . . . 6 ((a ∪ b) ∩ b) = b
24	18, 23	2or 67	. . . . 5 (((a ∪ b) ∩ b⊥ ) ∪ ((a ∪ b) ∩ b)) = ((a ∩ b⊥ ) ∪ b)
25	6, 7, 24	3tr 62	. . . 4 ((a ∪ b) ∩ (b ∪ b⊥ )) = ((a ∩ b⊥ ) ∪ b)
26	2, 3, 25	3tr2 61	. . 3 (a ∪ b) = ((a ∩ b⊥ ) ∪ b)
27	26	ran 71	. 2 ((a ∪ b) ∩ (b⊥ ∪ c)) = (((a ∩ b⊥ ) ∪ b) ∩ (b⊥ ∪ c))
28		comorr 176	. . . . 5 b⊥ C (b⊥ ∪ c)
29	28	comcom6 441	. . . 4 b C (b⊥ ∪ 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⊥ ) ∪ b) ∩ (b⊥ ∪ c)) = (((a ∩ b⊥ ) ∩ (b⊥ ∪ c)) ∪ (b ∩ (b⊥ ∪ c)))
33		leao2 155	. . . . 5 (a ∩ b⊥ ) ≤ (b⊥ ∪ c)
34	33	df2le2 128	. . . 4 ((a ∩ b⊥ ) ∩ (b⊥ ∪ c)) = (a ∩ b⊥ )
35	34	ax-r5 37	. . 3 (((a ∩ b⊥ ) ∩ (b⊥ ∪ c)) ∪ (b ∩ (b⊥ ∪ c))) = ((a ∩ b⊥ ) ∪ (b ∩ (b⊥ ∪ c)))
36	32, 35	ax-r2 35	. 2 (((a ∩ b⊥ ) ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ (b⊥ ∪ 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⊥ ∪ c)) = ((b ∩ b⊥ ) ∪ (b ∩ c))
41	14	ax-r5 37	. . . . 5 (0 ∪ (b ∩ c)) = ((b ∩ b⊥ ) ∪ (b ∩ c))
42	41	ax-r1 34	. . . 4 ((b ∩ b⊥ ) ∪ (b ∩ c)) = (0 ∪ (b ∩ c))
43		or0r 95	. . . 4 (0 ∪ (b ∩ c)) = (b ∩ c)
44	40, 42, 43	3tr 62	. . 3 (b ∩ (b⊥ ∪ c)) = (b ∩ c)
45	44	lor 66	. 2 ((a ∩ b⊥ ) ∪ (b ∩ (b⊥ ∪ c))) = ((a ∩ b⊥ ) ∪ (b ∩ c))
46	27, 36, 45	3tr 62	1 ((a ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ c))

Syntax hints:   = wb 1   C wc 3  ^⊥ wn 4   ∪ 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