Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oaliii 981

Description: Orthoarguesian law. Godowski/Greechie, Eq. III.

**Assertion**
Ref	Expression
oaliii	((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))

**Proof of Theorem oaliii**
Step	Hyp	Ref	Expression
1		anass 69	. . . . 5 (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂b) ∩ (((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))
2		anidm 103	. . . . . 6 (((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))
3	2	lan 70	. . . . 5 ((a →₂b) ∩ (((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))) = ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
4	1, 3	ax-r2 35	. . . 4 (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
5	4	ax-r1 34	. . 3 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
6		oal2 979	. . . 4 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ (a →₂c)
7	6	leran 145	. . 3 (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
8	5, 7	bltr 130	. 2 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
9		anass 69	. . . . 5 (((a →₂c) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂c) ∩ (((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))))
10		ax-a2 30	. . . . . . . . . 10 (c ∪ b) = (b ∪ c)
11	10	ax-r4 36	. . . . . . . . 9 (c ∪ b)^⊥ = (b ∪ c)^⊥
12		ancom 68	. . . . . . . . 9 ((a →₂c) ∩ (a →₂b)) = ((a →₂b) ∩ (a →₂c))
13	11, 12	2or 67	. . . . . . . 8 ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))) = ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))
14	13	ran 71	. . . . . . 7 (((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = (((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
15	14, 2	ax-r2 35	. . . . . 6 (((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))
16	15	lan 70	. . . . 5 ((a →₂c) ∩ (((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))) = ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
17	9, 16	ax-r2 35	. . . 4 (((a →₂c) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
18	17	ax-r1 34	. . 3 ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = (((a →₂c) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
19		oal2 979	. . . 4 ((a →₂c) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ≤ (a →₂b)
20	19	leran 145	. . 3 (((a →₂c) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
21	18, 20	bltr 130	. 2 ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))
22	8, 21	lebi 137	1 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂c) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))))

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₂wi2 14

This theorem is referenced by: oalii 982 oath1 984

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-3oa 978

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

metamath.org