Theorem k1-5 360

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

Hypotheses

Ref	Expression
k1-5.1	(x⊥ ∩ (x ∪ c)) = (((x⊥ ∩ (x ∪ c)) ∩ c) ∪ ((x⊥ ∩ (x ∪ c)) ∩ c⊥ ))
k1-5.2	x ≤ c⊥

Assertion

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

Proof of Theorem k1-5

Step	Hyp	Ref	Expression
1		k1-5.1	. . 3 (x⊥ ∩ (x ∪ c)) = (((x⊥ ∩ (x ∪ c)) ∩ c) ∪ ((x⊥ ∩ (x ∪ c)) ∩ c⊥ ))
2		ax-a1 30	. . . . 5 c = c⊥ ⊥
3	2	lor 70	. . . 4 (x ∪ c) = (x ∪ c⊥ ⊥ )
4	3	lan 77	. . 3 (x⊥ ∩ (x ∪ c)) = (x⊥ ∩ (x ∪ c⊥ ⊥ ))
5		orcom 73	. . . 4 (((x⊥ ∩ (x ∪ c)) ∩ c) ∪ ((x⊥ ∩ (x ∪ c)) ∩ c⊥ )) = (((x⊥ ∩ (x ∪ c)) ∩ c⊥ ) ∪ ((x⊥ ∩ (x ∪ c)) ∩ c))
6	4	ran 78	. . . . 5 ((x⊥ ∩ (x ∪ c)) ∩ c⊥ ) = ((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ )
7	4, 2	2an 79	. . . . 5 ((x⊥ ∩ (x ∪ c)) ∩ c) = ((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ ⊥ )
8	6, 7	2or 72	. . . 4 (((x⊥ ∩ (x ∪ c)) ∩ c⊥ ) ∪ ((x⊥ ∩ (x ∪ c)) ∩ c)) = (((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ ) ∪ ((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ ⊥ ))
9	5, 8	tr 62	. . 3 (((x⊥ ∩ (x ∪ c)) ∩ c) ∪ ((x⊥ ∩ (x ∪ c)) ∩ c⊥ )) = (((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ ) ∪ ((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ ⊥ ))
10	1, 4, 9	3tr2 64	. 2 (x⊥ ∩ (x ∪ c⊥ ⊥ )) = (((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ ) ∪ ((x⊥ ∩ (x ∪ c⊥ ⊥ )) ∩ c⊥ ⊥ ))
11		k1-5.2	. 2 x ≤ c⊥
12	10, 11	k1-4 359	1 (x ∪ (x⊥ ∩ c⊥ )) = c⊥

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ 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  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by: (None)