Theorem k1-3 358

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

Hypotheses

Ref	Expression
k1-3.1	x = ((x ∩ c) ∪ (x ∩ c⊥ ))
k1-3.2	y = ((y ∩ c) ∪ (y ∩ c⊥ ))
k1-3.3	((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))⊥ = ((((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))⊥ ∩ c) ∪ (((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))⊥ ∩ c⊥ ))

Assertion

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

Proof of Theorem k1-3

Step	Hyp	Ref	Expression
1		k1-3.1	. . . . 5 x = ((x ∩ c) ∪ (x ∩ c⊥ ))
2		k1-3.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-3.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-8b 356	. . 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⊥ ))

Syntax hints:   = wb 1  ^⊥ 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)