Theorem k1-2 357

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

Hypotheses

Ref	Expression
k1-2.1	x = ((x ∩ c) ∪ (x ∩ c⊥ ))
k1-2.2	y = ((y ∩ c) ∪ (y ∩ c⊥ ))
k1-2.3	((x ∩ c) ∪ (y ∩ c))⊥ = ((((x ∩ c) ∪ (y ∩ c))⊥ ∩ c) ∪ (((x ∩ c) ∪ (y ∩ c))⊥ ∩ c⊥ ))

Assertion

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

Proof of Theorem k1-2

Step	Hyp	Ref	Expression
1		k1-2.1	. . . . 5 x = ((x ∩ c) ∪ (x ∩ c⊥ ))
2		k1-2.2	. . . . 5 y = ((y ∩ c) ∪ (y ∩ c⊥ ))
3	1, 2	2or 72	. . . 4 (x ∪ y) = (((x ∩ c) ∪ (x ∩ c⊥ )) ∪ ((y ∩ c) ∪ (y ∩ c⊥ )))
4		or4 84	. . . 4 (((x ∩ c) ∪ (x ∩ c⊥ )) ∪ ((y ∩ c) ∪ (y ∩ c⊥ ))) = (((x ∩ c) ∪ (y ∩ c)) ∪ ((x ∩ c⊥ ) ∪ (y ∩ c⊥ )))
5	3, 4	ax-r2 36	. . 3 (x ∪ y) = (((x ∩ c) ∪ (y ∩ c)) ∪ ((x ∩ c⊥ ) ∪ (y ∩ c⊥ )))
6	5	ran 78	. 2 ((x ∪ y) ∩ c) = ((((x ∩ c) ∪ (y ∩ c)) ∪ ((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))) ∩ c)
7		k1-2.3	. . . 4 ((x ∩ c) ∪ (y ∩ c))⊥ = ((((x ∩ c) ∪ (y ∩ c))⊥ ∩ c) ∪ (((x ∩ c) ∪ (y ∩ c))⊥ ∩ c⊥ ))
8		lear 161	. . . . 5 (x ∩ c) ≤ c
9		lear 161	. . . . 5 (y ∩ c) ≤ c
10	8, 9	lel2or 170	. . . 4 ((x ∩ c) ∪ (y ∩ c)) ≤ c
11		lear 161	. . . . 5 (x ∩ c⊥ ) ≤ c⊥
12		lear 161	. . . . 5 (y ∩ c⊥ ) ≤ c⊥
13	11, 12	lel2or 170	. . . 4 ((x ∩ c⊥ ) ∪ (y ∩ c⊥ )) ≤ c⊥
14	7, 10, 13	k1-8a 355	. . 3 ((x ∩ c) ∪ (y ∩ c)) = ((((x ∩ c) ∪ (y ∩ c)) ∪ ((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))) ∩ c)
15	14	ax-r1 35	. 2 ((((x ∩ c) ∪ (y ∩ c)) ∪ ((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))) ∩ c) = ((x ∩ c) ∪ (y ∩ c))
16	6, 15	tr 62	1 ((x ∪ y) ∩ c) = ((x ∩ c) ∪ (y ∩ 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  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by: (None)