Theorem k1-4 359

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

Hypotheses

Ref	Expression
k1-4.1	(x⊥ ∩ (x ∪ c⊥ )) = (((x⊥ ∩ (x ∪ c⊥ )) ∩ c) ∪ ((x⊥ ∩ (x ∪ c⊥ )) ∩ c⊥ ))
k1-4.2	x ≤ c

Assertion

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

Proof of Theorem k1-4

Step	Hyp	Ref	Expression
1		oran1 91	. . . . 5 (x ∪ c⊥ ) = (x⊥ ∩ c)⊥
2	1	lan 77	. . . 4 (x⊥ ∩ (x ∪ c⊥ )) = (x⊥ ∩ (x⊥ ∩ c)⊥ )
3	2	cm 61	. . 3 (x⊥ ∩ (x⊥ ∩ c)⊥ ) = (x⊥ ∩ (x ∪ c⊥ ))
4		anor3 90	. . 3 (x⊥ ∩ (x⊥ ∩ c)⊥ ) = (x ∪ (x⊥ ∩ c))⊥
5		k1-4.1	. . . 4 (x⊥ ∩ (x ∪ c⊥ )) = (((x⊥ ∩ (x ∪ c⊥ )) ∩ c) ∪ ((x⊥ ∩ (x ∪ c⊥ )) ∩ c⊥ ))
6	1	lan 77	. . . . . 6 ((x⊥ ∩ c) ∩ (x ∪ c⊥ )) = ((x⊥ ∩ c) ∩ (x⊥ ∩ c)⊥ )
7		an32 83	. . . . . 6 ((x⊥ ∩ (x ∪ c⊥ )) ∩ c) = ((x⊥ ∩ c) ∩ (x ∪ c⊥ ))
8		dff 101	. . . . . 6 0 = ((x⊥ ∩ c) ∩ (x⊥ ∩ c)⊥ )
9	6, 7, 8	3tr1 63	. . . . 5 ((x⊥ ∩ (x ∪ c⊥ )) ∩ c) = 0
10		an32 83	. . . . . 6 ((x⊥ ∩ (x ∪ c⊥ )) ∩ c⊥ ) = ((x⊥ ∩ c⊥ ) ∩ (x ∪ c⊥ ))
11		leao4 165	. . . . . . 7 (x⊥ ∩ c⊥ ) ≤ (x ∪ c⊥ )
12	11	df2le2 136	. . . . . 6 ((x⊥ ∩ c⊥ ) ∩ (x ∪ c⊥ )) = (x⊥ ∩ c⊥ )
13		anor3 90	. . . . . . 7 (x⊥ ∩ c⊥ ) = (x ∪ c)⊥
14		k1-4.2	. . . . . . . . 9 x ≤ c
15	14	df-le2 131	. . . . . . . 8 (x ∪ c) = c
16	15	ax-r4 37	. . . . . . 7 (x ∪ c)⊥ = c⊥
17	13, 16	tr 62	. . . . . 6 (x⊥ ∩ c⊥ ) = c⊥
18	10, 12, 17	3tr 65	. . . . 5 ((x⊥ ∩ (x ∪ c⊥ )) ∩ c⊥ ) = c⊥
19	9, 18	2or 72	. . . 4 (((x⊥ ∩ (x ∪ c⊥ )) ∩ c) ∪ ((x⊥ ∩ (x ∪ c⊥ )) ∩ c⊥ )) = (0 ∪ c⊥ )
20		or0r 103	. . . 4 (0 ∪ c⊥ ) = c⊥
21	5, 19, 20	3tr 65	. . 3 (x⊥ ∩ (x ∪ c⊥ )) = c⊥
22	3, 4, 21	3tr2 64	. 2 (x ∪ (x⊥ ∩ c))⊥ = c⊥
23	22	con1 66	1 (x ∪ (x⊥ ∩ c)) = c

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 9

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  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by:  k1-5  360