Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oalem1 985

Description: Lemma

**Assertion**
Ref	Expression
oalem1	((b ∪ c) ∪ ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))))) ≤ (a →₂(b ∪ c))

**Proof of Theorem oalem1**
Step	Hyp	Ref	Expression
1		anidm 103	. . . . . . . . 9 (b^⊥ ∩ b^⊥ ) = b^⊥
2	1	ran 71	. . . . . . . 8 ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = (b^⊥ ∩ c^⊥ )
3	2	ax-r1 34	. . . . . . 7 (b^⊥ ∩ c^⊥ ) = ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ )
4		anor3 82	. . . . . . 7 (b^⊥ ∩ c^⊥ ) = (b ∪ c)^⊥
5		an32 76	. . . . . . . 8 ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = ((b^⊥ ∩ c^⊥ ) ∩ b^⊥ )
6	4	ran 71	. . . . . . . 8 ((b^⊥ ∩ c^⊥ ) ∩ b^⊥ ) = ((b ∪ c)^⊥ ∩ b^⊥ )
7	5, 6	ax-r2 35	. . . . . . 7 ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = ((b ∪ c)^⊥ ∩ b^⊥ )
8	3, 4, 7	3tr2 61	. . . . . 6 (b ∪ c)^⊥ = ((b ∪ c)^⊥ ∩ b^⊥ )
9	8	ran 71	. . . . 5 ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) = (((b ∪ c)^⊥ ∩ b^⊥ ) ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))))
10		anass 69	. . . . . 6 (((b ∪ c)^⊥ ∩ b^⊥ ) ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) = ((b ∪ c)^⊥ ∩ (b^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))))
11		oalii 982	. . . . . . 7 (b^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ a^⊥
12	11	lelan 159	. . . . . 6 ((b ∪ c)^⊥ ∩ (b^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))))) ≤ ((b ∪ c)^⊥ ∩ a^⊥ )
13	10, 12	bltr 130	. . . . 5 (((b ∪ c)^⊥ ∩ b^⊥ ) ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ ((b ∪ c)^⊥ ∩ a^⊥ )
14	9, 13	bltr 130	. . . 4 ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ ((b ∪ c)^⊥ ∩ a^⊥ )
15		ancom 68	. . . 4 ((b ∪ c)^⊥ ∩ a^⊥ ) = (a^⊥ ∩ (b ∪ c)^⊥ )
16	14, 15	lbtr 131	. . 3 ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ (a^⊥ ∩ (b ∪ c)^⊥ )
17	16	lelor 158	. 2 ((b ∪ c) ∪ ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))))) ≤ ((b ∪ c) ∪ (a^⊥ ∩ (b ∪ c)^⊥ ))
18		df-i2 44	. . 3 (a →₂(b ∪ c)) = ((b ∪ c) ∪ (a^⊥ ∩ (b ∪ c)^⊥ ))
19	18	ax-r1 34	. 2 ((b ∪ c) ∪ (a^⊥ ∩ (b ∪ c)^⊥ )) = (a →₂(b ∪ c))
20	17, 19	lbtr 131	1 ((b ∪ c) ∪ ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))))) ≤ (a →₂(b ∪ c))

Colors of variables: term

Syntax hints: ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₂wi2 14

This theorem was proved from axioms: ax-a1 29 ax-a2 30 ax-a3 31 ax-a5 33 ax-r1 34 ax-r2 35 ax-r4 36 ax-r5 37 ax-r3 421 ax-3oa 978

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i1 43 df-i2 44 df-le1 122 df-le2 123

metamath.org