Theorem k1-8a 355

Description: First part of statement (8) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 27-May-2008.)

Hypotheses

Ref	Expression
k1-8a.1	x⊥ = ((x⊥ ∩ c) ∪ (x⊥ ∩ c⊥ ))
k1-8a.2	x ≤ c
k1-8a.3	y ≤ c⊥

Assertion

Ref	Expression
k1-8a	x = ((x ∪ y) ∩ c)

Proof of Theorem k1-8a

Step	Hyp	Ref	Expression
1		leo 158	. . 3 x ≤ (x ∪ y)
2		k1-8a.2	. . 3 x ≤ c
3	1, 2	ler2an 173	. 2 x ≤ ((x ∪ y) ∩ c)
4		k1-8a.3	. . . . 5 y ≤ c⊥
5	4	lelor 166	. . . 4 (x ∪ y) ≤ (x ∪ c⊥ )
6	5	leran 153	. . 3 ((x ∪ y) ∩ c) ≤ ((x ∪ c⊥ ) ∩ c)
7		ax-a1 30	. . . . . 6 x = x⊥ ⊥
8	7	ror 71	. . . . 5 (x ∪ c⊥ ) = (x⊥ ⊥ ∪ c⊥ )
9	8	ran 78	. . . 4 ((x ∪ c⊥ ) ∩ c) = ((x⊥ ⊥ ∪ c⊥ ) ∩ c)
10	7	ran 78	. . . . . 6 (x ∩ c) = (x⊥ ⊥ ∩ c)
11		k1-8a.1	. . . . . . 7 x⊥ = ((x⊥ ∩ c) ∪ (x⊥ ∩ c⊥ ))
12	11	k1-6 353	. . . . . 6 (x⊥ ⊥ ∩ c) = ((x⊥ ⊥ ∪ c⊥ ) ∩ c)
13	10, 12	tr 62	. . . . 5 (x ∩ c) = ((x⊥ ⊥ ∪ c⊥ ) ∩ c)
14	13	cm 61	. . . 4 ((x⊥ ⊥ ∪ c⊥ ) ∩ c) = (x ∩ c)
15	2	df2le2 136	. . . 4 (x ∩ c) = x
16	9, 14, 15	3tr 65	. . 3 ((x ∪ c⊥ ) ∩ c) = x
17	6, 16	lbtr 139	. 2 ((x ∪ y) ∩ c) ≤ x
18	3, 17	lebi 145	1 x = ((x ∪ y) ∩ c)

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ 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  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by:  k1-8b  356  k1-2  357