oa23 - Quantum Logic Explorer

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

Theorem oa23 936

Description: Derivation of OA from Godowski/Greechie Eq. II. (Contributed by NM, 25-Nov-1998.)

**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 31	. . . . . . 7 (b ∪ c) = (c ∪ b)
2	1	ax-r4 37	. . . . . 6 (b ∪ c)^⊥ = (c ∪ b)^⊥
3		ancom 74	. . . . . 6 ((a →₂b) ∩ (a →₂c)) = ((a →₂c) ∩ (a →₂b))
4	2, 3	2or 72	. . . . 5 ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c))) = ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))
5	4	lan 77	. . . 4 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) = ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))
6	5	ax-r5 38	. . 3 (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∪ (a →₂c)) = (((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∪ (a →₂c))
7		ax-a2 31	. . 3 (((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))) ∪ (a →₂c)) = ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
8		ax-a3 32	. . . . . . . . . 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 35	. . . . . . . . 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 110	. . . . . . . . . 10 ((a →₂c) ∪ (a →₂c)) = (a →₂c)
11	10	ax-r5 38	. . . . . . . . 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 36	. . . . . . . 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 636	. . . . . . . 8 ((a →₂c) ∪ c^⊥ ) = 1
14	12, 13	2an 79	. . . . . . 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 35	. . . . . 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 106	. . . . . . 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 35	. . . . . 6 ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) = (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ 1)
18		comorr 184	. . . . . . 7 (a →₂c) C ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
19		u2lemc1 681	. . . . . . . . 9 c C (a →₂c)
20	19	comcom 453	. . . . . . . 8 (a →₂c) C c
21	20	comcom2 183	. . . . . . 7 (a →₂c) C c^⊥
22	18, 21	fh3 471	. . . . . 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 63	. . . . 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 160	. . . . . . . . 9 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ c^⊥
26	24, 25	ler2an 173	. . . . . . . 8 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ (a^⊥ ∩ c^⊥ )
27		ancom 74	. . . . . . . 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 616	. . . . . . . 8 ((a →₂c) ∩ c^⊥ ) = (a^⊥ ∩ c^⊥ )
29	26, 27, 28	le3tr1 140	. . . . . . 7 (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ ) ≤ ((a →₂c) ∩ c^⊥ )
30	29	lelor 166	. . . . . 6 ((a →₂c) ∪ (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ )) ≤ ((a →₂c) ∪ ((a →₂c) ∩ c^⊥ ))
31		orabs 120	. . . . . 6 ((a →₂c) ∪ ((a →₂c) ∩ c^⊥ )) = (a →₂c)
32	30, 31	lbtr 139	. . . . 5 ((a →₂c) ∪ (((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ∩ c^⊥ )) ≤ (a →₂c)
33	23, 32	bltr 138	. . . 4 ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) ≤ (a →₂c)
34		leo 158	. . . 4 (a →₂c) ≤ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))
35	33, 34	lebi 145	. . 3 ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b))))) = (a →₂c)
36	6, 7, 35	3tr 65	. 2 (((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ∪ (a →₂c)) = (a →₂c)
37	36	df-le1 130	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 8 →₂wi2 13

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

This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i2 45 df-le1 130 df-le2 131 df-c1 132 df-c2 133

This theorem is referenced by: oa43v 1028 oa63v 1032

W3C validator