Theorem k1-7 354

Description: Statement (7) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 26-May-2008.)

Hypothesis

Ref	Expression
k1-7.1	x = ((x ∩ c) ∪ (x ∩ c⊥ ))

Assertion

Ref	Expression
k1-7	(x⊥ ∩ c⊥ ) = ((x⊥ ∪ c) ∩ c⊥ )

Proof of Theorem k1-7

Step	Hyp	Ref	Expression
1		anor3 90	. . . . 5 ((x ∩ c⊥ )⊥ ∩ (x ∩ c⊥ ⊥ )⊥ ) = ((x ∩ c⊥ ) ∪ (x ∩ c⊥ ⊥ ))⊥
2	1	cm 61	. . . 4 ((x ∩ c⊥ ) ∪ (x ∩ c⊥ ⊥ ))⊥ = ((x ∩ c⊥ )⊥ ∩ (x ∩ c⊥ ⊥ )⊥ )
3		k1-7.1	. . . . . 6 x = ((x ∩ c) ∪ (x ∩ c⊥ ))
4		ax-a1 30	. . . . . . . 8 c = c⊥ ⊥
5	4	lan 77	. . . . . . 7 (x ∩ c) = (x ∩ c⊥ ⊥ )
6	5	ror 71	. . . . . 6 ((x ∩ c) ∪ (x ∩ c⊥ )) = ((x ∩ c⊥ ⊥ ) ∪ (x ∩ c⊥ ))
7		orcom 73	. . . . . 6 ((x ∩ c⊥ ⊥ ) ∪ (x ∩ c⊥ )) = ((x ∩ c⊥ ) ∪ (x ∩ c⊥ ⊥ ))
8	3, 6, 7	3tr 65	. . . . 5 x = ((x ∩ c⊥ ) ∪ (x ∩ c⊥ ⊥ ))
9	8	con4 69	. . . 4 x⊥ = ((x ∩ c⊥ ) ∪ (x ∩ c⊥ ⊥ ))⊥
10		oran3 93	. . . . 5 (x⊥ ∪ c⊥ ⊥ ) = (x ∩ c⊥ )⊥
11		oran2 92	. . . . 5 (x⊥ ∪ c⊥ ) = (x ∩ c⊥ ⊥ )⊥
12	10, 11	2an 79	. . . 4 ((x⊥ ∪ c⊥ ⊥ ) ∩ (x⊥ ∪ c⊥ )) = ((x ∩ c⊥ )⊥ ∩ (x ∩ c⊥ ⊥ )⊥ )
13	2, 9, 12	3tr1 63	. . 3 x⊥ = ((x⊥ ∪ c⊥ ⊥ ) ∩ (x⊥ ∪ c⊥ ))
14	13	ran 78	. 2 (x⊥ ∩ c⊥ ) = (((x⊥ ∪ c⊥ ⊥ ) ∩ (x⊥ ∪ c⊥ )) ∩ c⊥ )
15	4	lor 70	. . . . . 6 (x⊥ ∪ c) = (x⊥ ∪ c⊥ ⊥ )
16	15	ran 78	. . . . 5 ((x⊥ ∪ c) ∩ (x⊥ ∪ c⊥ )) = ((x⊥ ∪ c⊥ ⊥ ) ∩ (x⊥ ∪ c⊥ ))
17	16	ran 78	. . . 4 (((x⊥ ∪ c) ∩ (x⊥ ∪ c⊥ )) ∩ c⊥ ) = (((x⊥ ∪ c⊥ ⊥ ) ∩ (x⊥ ∪ c⊥ )) ∩ c⊥ )
18	17	cm 61	. . 3 (((x⊥ ∪ c⊥ ⊥ ) ∩ (x⊥ ∪ c⊥ )) ∩ c⊥ ) = (((x⊥ ∪ c) ∩ (x⊥ ∪ c⊥ )) ∩ c⊥ )
19		anass 76	. . 3 (((x⊥ ∪ c) ∩ (x⊥ ∪ c⊥ )) ∩ c⊥ ) = ((x⊥ ∪ c) ∩ ((x⊥ ∪ c⊥ ) ∩ c⊥ ))
20	18, 19	tr 62	. 2 (((x⊥ ∪ c⊥ ⊥ ) ∩ (x⊥ ∪ c⊥ )) ∩ c⊥ ) = ((x⊥ ∪ c) ∩ ((x⊥ ∪ c⊥ ) ∩ c⊥ ))
21		ancom 74	. . . 4 ((x⊥ ∪ c⊥ ) ∩ c⊥ ) = (c⊥ ∩ (x⊥ ∪ c⊥ ))
22		ax-a2 31	. . . . 5 (x⊥ ∪ c⊥ ) = (c⊥ ∪ x⊥ )
23	22	lan 77	. . . 4 (c⊥ ∩ (x⊥ ∪ c⊥ )) = (c⊥ ∩ (c⊥ ∪ x⊥ ))
24		anabs 121	. . . 4 (c⊥ ∩ (c⊥ ∪ x⊥ )) = c⊥
25	21, 23, 24	3tr 65	. . 3 ((x⊥ ∪ c⊥ ) ∩ c⊥ ) = c⊥
26	25	lan 77	. 2 ((x⊥ ∪ c) ∩ ((x⊥ ∪ c⊥ ) ∩ c⊥ )) = ((x⊥ ∪ c) ∩ c⊥ )
27	14, 20, 26	3tr 65	1 (x⊥ ∩ c⊥ ) = ((x⊥ ∪ c) ∩ c⊥ )

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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

This theorem depends on definitions:  df-a 40

This theorem is referenced by: (None)