Theorem k1-6 353

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

Hypothesis

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

Assertion

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

Proof of Theorem k1-6

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-6.1	. . . . 5 x = ((x ∩ c) ∪ (x ∩ c⊥ ))
4	3	con4 69	. . . 4 x⊥ = ((x ∩ c) ∪ (x ∩ c⊥ ))⊥
5		oran3 93	. . . . 5 (x⊥ ∪ c⊥ ) = (x ∩ c)⊥
6		oran2 92	. . . . 5 (x⊥ ∪ c) = (x ∩ c⊥ )⊥
7	5, 6	2an 79	. . . 4 ((x⊥ ∪ c⊥ ) ∩ (x⊥ ∪ c)) = ((x ∩ c)⊥ ∩ (x ∩ c⊥ )⊥ )
8	2, 4, 7	3tr1 63	. . 3 x⊥ = ((x⊥ ∪ c⊥ ) ∩ (x⊥ ∪ c))
9	8	ran 78	. 2 (x⊥ ∩ c) = (((x⊥ ∪ c⊥ ) ∩ (x⊥ ∪ c)) ∩ c)
10		anass 76	. 2 (((x⊥ ∪ c⊥ ) ∩ (x⊥ ∪ c)) ∩ c) = ((x⊥ ∪ c⊥ ) ∩ ((x⊥ ∪ c) ∩ c))
11		ancom 74	. . . 4 ((x⊥ ∪ c) ∩ c) = (c ∩ (x⊥ ∪ c))
12		ax-a2 31	. . . . 5 (x⊥ ∪ c) = (c ∪ x⊥ )
13	12	lan 77	. . . 4 (c ∩ (x⊥ ∪ c)) = (c ∩ (c ∪ x⊥ ))
14		anabs 121	. . . 4 (c ∩ (c ∪ x⊥ )) = c
15	11, 13, 14	3tr 65	. . 3 ((x⊥ ∪ c) ∩ c) = c
16	15	lan 77	. 2 ((x⊥ ∪ c⊥ ) ∩ ((x⊥ ∪ c) ∩ c)) = ((x⊥ ∪ c⊥ ) ∩ c)
17	9, 10, 16	3tr 65	1 (x⊥ ∩ c) = ((x⊥ ∪ c⊥ ) ∩ c)

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This proof depends on 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 proof depends on definitions:  df-a 40

This theorem is used by:  k1-8a  355