Theorem marsdenlem2 881

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

Hypotheses

Ref	Expression
marsden.1	a C b
marsden.2	b C c
marsden.3	c C d
marsden.4	d C a

Assertion

Ref	Expression
marsdenlem2	((c ∪ d) ∩ (b⊥ ∪ c⊥ )) = (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∪ (b⊥ ∩ d))

Proof of Theorem marsdenlem2

Step	Hyp	Ref	Expression
1		ancom 74	. 2 ((c ∪ d) ∩ (b⊥ ∪ c⊥ )) = ((b⊥ ∪ c⊥ ) ∩ (c ∪ d))
2		comorr 184	. . . 4 c C (c ∪ d)
3	2	comcom3 454	. . 3 c⊥ C (c ∪ d)
4		marsden.2	. . . . 5 b C c
5	4	comcom4 455	. . . 4 b⊥ C c⊥
6	5	comcom 453	. . 3 c⊥ C b⊥
7	3, 6	fh2rc 480	. 2 ((b⊥ ∪ c⊥ ) ∩ (c ∪ d)) = ((b⊥ ∩ (c ∪ d)) ∪ (c⊥ ∩ (c ∪ d)))
8	6	comcom6 459	. . . . 5 c C b⊥
9		marsden.3	. . . . 5 c C d
10	8, 9	fh2 470	. . . 4 (b⊥ ∩ (c ∪ d)) = ((b⊥ ∩ c) ∪ (b⊥ ∩ d))
11		comid 187	. . . . . . 7 c C c
12	11	comcom2 183	. . . . . 6 c C c⊥
13	12, 9	fh2 470	. . . . 5 (c⊥ ∩ (c ∪ d)) = ((c⊥ ∩ c) ∪ (c⊥ ∩ d))
14		dff 101	. . . . . . . 8 0 = (c ∩ c⊥ )
15		ancom 74	. . . . . . . 8 (c ∩ c⊥ ) = (c⊥ ∩ c)
16	14, 15	ax-r2 36	. . . . . . 7 0 = (c⊥ ∩ c)
17	16	ax-r5 38	. . . . . 6 (0 ∪ (c⊥ ∩ d)) = ((c⊥ ∩ c) ∪ (c⊥ ∩ d))
18	17	ax-r1 35	. . . . 5 ((c⊥ ∩ c) ∪ (c⊥ ∩ d)) = (0 ∪ (c⊥ ∩ d))
19		or0r 103	. . . . 5 (0 ∪ (c⊥ ∩ d)) = (c⊥ ∩ d)
20	13, 18, 19	3tr 65	. . . 4 (c⊥ ∩ (c ∪ d)) = (c⊥ ∩ d)
21	10, 20	2or 72	. . 3 ((b⊥ ∩ (c ∪ d)) ∪ (c⊥ ∩ (c ∪ d))) = (((b⊥ ∩ c) ∪ (b⊥ ∩ d)) ∪ (c⊥ ∩ d))
22		or32 82	. . 3 (((b⊥ ∩ c) ∪ (b⊥ ∩ d)) ∪ (c⊥ ∩ d)) = (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∪ (b⊥ ∩ d))
23	21, 22	ax-r2 36	. 2 ((b⊥ ∩ (c ∪ d)) ∪ (c⊥ ∩ (c ∪ d))) = (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∪ (b⊥ ∩ d))
24	1, 7, 23	3tr 65	1 ((c ∪ d) ∩ (b⊥ ∪ c⊥ )) = (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∪ (b⊥ ∩ d))

This proof depends on syntax axioms:   = wb 1   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  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: (None)