Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa23 916

Description: Derivation of OA from Godowski/Greechie Eq. II.

**Hypothesis**
Ref	Expression
oa23.1	(c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ a^⊥

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

**Proof of Theorem oa23**
Step	Hyp	Ref	Expression
1		ax-a2 30	. . . . . . 7 (b ∪ c) = (c ∪ b)
2	1	ax-r4 36	. . . . . 6 (b ∪ c)^⊥ = (c ∪ b)^⊥
3		ancom 68	. . . . . 6 ((a →₂b) ∩ (a →₂c)) = ((a →₂c) ∩ (a →₂b))
4	2, 3	2or 67	. . . . 5 ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))) = ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))
5	4	lan 70	. . . 4 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))
6	5	ax-r5 37	. . 3 (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∪ (a →₂c)) = (((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∪ (a →₂c))
7		ax-a2 30	. . 3 (((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∪ (a →₂c)) = ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
8		ax-a3 31	. . . . . . . . . 10 (((a →₂c) ∪ (a →₂c)) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) = ((a →₂c) ∪ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))))
9	8	ax-r1 34	. . . . . . . . 9 ((a →₂c) ∪ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) = (((a →₂c) ∪ (a →₂c)) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
10		oridm 102	. . . . . . . . . 10 ((a →₂c) ∪ (a →₂c)) = (a →₂c)
11	10	ax-r5 37	. . . . . . . . 9 (((a →₂c) ∪ (a →₂c)) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) = ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
12	9, 11	ax-r2 35	. . . . . . . 8 ((a →₂c) ∪ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) = ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
13		u2lemonb 618	. . . . . . . 8 ((a →₂c) ∪ c^⊥ ) = 1
14	12, 13	2an 72	. . . . . . 7 (((a →₂c) ∪ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ∩ ((a →₂c) ∪ c^⊥ )) = (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ 1)
15	14	ax-r1 34	. . . . . 6 (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ 1) = (((a →₂c) ∪ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ∩ ((a →₂c) ∪ c^⊥ ))
16		an1 98	. . . . . . 7 (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ 1) = ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
17	16	ax-r1 34	. . . . . 6 ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) = (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ 1)
18		comorr 176	. . . . . . 7 (a →₂c) C ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
19		u2lemc1 663	. . . . . . . . 9 c C (a →₂c)
20	19	comcom 435	. . . . . . . 8 (a →₂c) C c
21	20	comcom2 175	. . . . . . 7 (a →₂c) C c^⊥
22	18, 21	fh3 453	. . . . . 6 ((a →₂c) ∪ (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ )) = (((a →₂c) ∪ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ∩ ((a →₂c) ∪ c^⊥ ))
23	15, 17, 22	3tr1 60	. . . . 5 ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) = ((a →₂c) ∪ (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ ))
24		oa23.1	. . . . . . . . 9 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ a^⊥
25		lea 152	. . . . . . . . 9 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ c^⊥
26	24, 25	ler2an 165	. . . . . . . 8 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ (a^⊥ ∩ c^⊥ )
27		ancom 68	. . . . . . . 8 (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ ) = (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))))
28		u2lemanb 598	. . . . . . . 8 ((a →₂c) ∩ c^⊥ ) = (a^⊥ ∩ c^⊥ )
29	26, 27, 28	le3tr1 132	. . . . . . 7 (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ ) ≤ ((a →₂c) ∩ c^⊥ )
30	29	lelor 158	. . . . . 6 ((a →₂c) ∪ (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ )) ≤ ((a →₂c) ∪ ((a →₂c) ∩ c^⊥ ))
31		a5b 112	. . . . . 6 ((a →₂c) ∪ ((a →₂c) ∩ c^⊥ )) = (a →₂c)
32	30, 31	lbtr 131	. . . . 5 ((a →₂c) ∪ (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ )) ≤ (a →₂c)
33	23, 32	bltr 130	. . . 4 ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ≤ (a →₂c)
34		leo 150	. . . 4 (a →₂c) ≤ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
35	33, 34	lebi 137	. . 3 ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) = (a →₂c)
36	6, 7, 35	3tr 62	. 2 (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∪ (a →₂c)) = (a →₂c)
37	36	df-le1 122	1 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ (a →₂c)

Colors of variables: term

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

This theorem is referenced by: oa43v 1008 oa63v 1011

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

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i2 44 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org