oalem1 - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > oalem1		GIF version

Theorem oalem1 1005

Description: Lemma. (Contributed by NM, 16-Oct-1998.)

**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 111	. . . . . . . . 9 (b^⊥ ∩ b^⊥ ) = b^⊥
2	1	ran 78	. . . . . . . 8 ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = (b^⊥ ∩ c^⊥ )
3	2	ax-r1 35	. . . . . . 7 (b^⊥ ∩ c^⊥ ) = ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ )
4		anor3 90	. . . . . . 7 (b^⊥ ∩ c^⊥ ) = (b ∪ c)^⊥
5		an32 83	. . . . . . . 8 ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = ((b^⊥ ∩ c^⊥ ) ∩ b^⊥ )
6	4	ran 78	. . . . . . . 8 ((b^⊥ ∩ c^⊥ ) ∩ b^⊥ ) = ((b ∪ c)^⊥ ∩ b^⊥ )
7	5, 6	ax-r2 36	. . . . . . 7 ((b^⊥ ∩ b^⊥ ) ∩ c^⊥ ) = ((b ∪ c)^⊥ ∩ b^⊥ )
8	3, 4, 7	3tr2 64	. . . . . 6 (b ∪ c)^⊥ = ((b ∪ c)^⊥ ∩ b^⊥ )
9	8	ran 78	. . . . 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 76	. . . . . 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 1002	. . . . . . 7 (b^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ a^⊥
12	11	lelan 167	. . . . . 6 ((b ∪ c)^⊥ ∩ (b^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))))) ≤ ((b ∪ c)^⊥ ∩ a^⊥ )
13	10, 12	bltr 138	. . . . 5 (((b ∪ c)^⊥ ∩ b^⊥ ) ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ ((b ∪ c)^⊥ ∩ a^⊥ )
14	9, 13	bltr 138	. . . 4 ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ ((b ∪ c)^⊥ ∩ a^⊥ )
15		ancom 74	. . . 4 ((b ∪ c)^⊥ ∩ a^⊥ ) = (a^⊥ ∩ (b ∪ c)^⊥ )
16	14, 15	lbtr 139	. . 3 ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))) ≤ (a^⊥ ∩ (b ∪ c)^⊥ )
17	16	lelor 166	. 2 ((b ∪ c) ∪ ((b ∪ c)^⊥ ∩ ((a →₂b) ∪ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))))) ≤ ((b ∪ c) ∪ (a^⊥ ∩ (b ∪ c)^⊥ ))
18		df-i2 45	. . 3 (a →₂(b ∪ c)) = ((b ∪ c) ∪ (a^⊥ ∩ (b ∪ c)^⊥ ))
19	18	ax-r1 35	. 2 ((b ∪ c) ∪ (a^⊥ ∩ (b ∪ c)^⊥ )) = (a →₂(b ∪ c))
20	17, 19	lbtr 139	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 13

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 ax-r3 439 ax-3oa 998

This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i1 44 df-i2 45 df-le1 130 df-le2 131

This theorem is referenced by: (None)

W3C validator