oa3-2to2s - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > oa3-2to2s		GIF version

Theorem oa3-2to2s 990

Description: Derivation of 3-OA variant from weaker version. (Contributed by NM, 25-Dec-1998.)

**Hypotheses**
Ref	Expression
oa3-2to2s.1	((a →₁d) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d)))))) ≤ d
oa3-2to2s.2	d = ((a ∩ c) ∪ (b ∩ c))

**Assertion**
Ref	Expression
oa3-2to2s	((a →₁c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))))) ≤ ((a ∩ c) ∪ (b ∩ c))

**Proof of Theorem oa3-2to2s**
Step	Hyp	Ref	Expression
1		id 59	. . 3 (a →₁c)^⊥ = (a →₁c)^⊥
2		id 59	. . 3 (b →₁c)^⊥ = (b →₁c)^⊥
3		id 59	. . 3 (0 →₁c)^⊥ = (0 →₁c)^⊥
4		leo 158	. . . . 5 a^⊥ ≤ (a^⊥ ∪ (a ∩ c))
5		df-i1 44	. . . . . . 7 (a →₁c) = (a^⊥ ∪ (a ∩ c))
6	5	ax-r1 35	. . . . . 6 (a^⊥ ∪ (a ∩ c)) = (a →₁c)
7		ax-a1 30	. . . . . 6 (a →₁c) = (a →₁c)^⊥ ^⊥
8	6, 7	ax-r2 36	. . . . 5 (a^⊥ ∪ (a ∩ c)) = (a →₁c)^⊥ ^⊥
9	4, 8	lbtr 139	. . . 4 a^⊥ ≤ (a →₁c)^⊥ ^⊥
10		leo 158	. . . . 5 b^⊥ ≤ (b^⊥ ∪ (b ∩ c))
11		df-i1 44	. . . . . . 7 (b →₁c) = (b^⊥ ∪ (b ∩ c))
12	11	ax-r1 35	. . . . . 6 (b^⊥ ∪ (b ∩ c)) = (b →₁c)
13		ax-a1 30	. . . . . 6 (b →₁c) = (b →₁c)^⊥ ^⊥
14	12, 13	ax-r2 36	. . . . 5 (b^⊥ ∪ (b ∩ c)) = (b →₁c)^⊥ ^⊥
15	10, 14	lbtr 139	. . . 4 b^⊥ ≤ (b →₁c)^⊥ ^⊥
16		leo 158	. . . . 5 0^⊥ ≤ (0^⊥ ∪ (0 ∩ c))
17		df-i1 44	. . . . . . 7 (0 →₁c) = (0^⊥ ∪ (0 ∩ c))
18	17	ax-r1 35	. . . . . 6 (0^⊥ ∪ (0 ∩ c)) = (0 →₁c)
19		ax-a1 30	. . . . . 6 (0 →₁c) = (0 →₁c)^⊥ ^⊥
20	18, 19	ax-r2 36	. . . . 5 (0^⊥ ∪ (0 ∩ c)) = (0 →₁c)^⊥ ^⊥
21	16, 20	lbtr 139	. . . 4 0^⊥ ≤ (0 →₁c)^⊥ ^⊥
22		or0 102	. . . . . 6 (d ∪ 0) = d
23	22	ax-r1 35	. . . . 5 d = (d ∪ 0)
24		oa3-2to2s.2	. . . . . . 7 d = ((a ∩ c) ∪ (b ∩ c))
25	5	lan 77	. . . . . . . . . . 11 (a ∩ (a →₁c)) = (a ∩ (a^⊥ ∪ (a ∩ c)))
26		omla 447	. . . . . . . . . . 11 (a ∩ (a^⊥ ∪ (a ∩ c))) = (a ∩ c)
27	25, 26	ax-r2 36	. . . . . . . . . 10 (a ∩ (a →₁c)) = (a ∩ c)
28	27	ax-r1 35	. . . . . . . . 9 (a ∩ c) = (a ∩ (a →₁c))
29		ax-a1 30	. . . . . . . . . 10 a = a^⊥ ^⊥
30	29, 7	2an 79	. . . . . . . . 9 (a ∩ (a →₁c)) = (a^⊥ ^⊥ ∩ (a →₁c)^⊥ ^⊥ )
31	28, 30	ax-r2 36	. . . . . . . 8 (a ∩ c) = (a^⊥ ^⊥ ∩ (a →₁c)^⊥ ^⊥ )
32	11	lan 77	. . . . . . . . . . 11 (b ∩ (b →₁c)) = (b ∩ (b^⊥ ∪ (b ∩ c)))
33		omla 447	. . . . . . . . . . 11 (b ∩ (b^⊥ ∪ (b ∩ c))) = (b ∩ c)
34	32, 33	ax-r2 36	. . . . . . . . . 10 (b ∩ (b →₁c)) = (b ∩ c)
35	34	ax-r1 35	. . . . . . . . 9 (b ∩ c) = (b ∩ (b →₁c))
36		ax-a1 30	. . . . . . . . . 10 b = b^⊥ ^⊥
37	36, 13	2an 79	. . . . . . . . 9 (b ∩ (b →₁c)) = (b^⊥ ^⊥ ∩ (b →₁c)^⊥ ^⊥ )
38	35, 37	ax-r2 36	. . . . . . . 8 (b ∩ c) = (b^⊥ ^⊥ ∩ (b →₁c)^⊥ ^⊥ )
39	31, 38	2or 72	. . . . . . 7 ((a ∩ c) ∪ (b ∩ c)) = ((a^⊥ ^⊥ ∩ (a →₁c)^⊥ ^⊥ ) ∪ (b^⊥ ^⊥ ∩ (b →₁c)^⊥ ^⊥ ))
40	24, 39	ax-r2 36	. . . . . 6 d = ((a^⊥ ^⊥ ∩ (a →₁c)^⊥ ^⊥ ) ∪ (b^⊥ ^⊥ ∩ (b →₁c)^⊥ ^⊥ ))
41		an1 106	. . . . . . . 8 (0 ∩ 1) = 0
42	41	ax-r1 35	. . . . . . 7 0 = (0 ∩ 1)
43		ax-a1 30	. . . . . . . 8 0 = 0^⊥ ^⊥
44		0i1 273	. . . . . . . . . 10 (0 →₁c) = 1
45	44	ax-r1 35	. . . . . . . . 9 1 = (0 →₁c)
46	45, 19	ax-r2 36	. . . . . . . 8 1 = (0 →₁c)^⊥ ^⊥
47	43, 46	2an 79	. . . . . . 7 (0 ∩ 1) = (0^⊥ ^⊥ ∩ (0 →₁c)^⊥ ^⊥ )
48	42, 47	ax-r2 36	. . . . . 6 0 = (0^⊥ ^⊥ ∩ (0 →₁c)^⊥ ^⊥ )
49	40, 48	2or 72	. . . . 5 (d ∪ 0) = (((a^⊥ ^⊥ ∩ (a →₁c)^⊥ ^⊥ ) ∪ (b^⊥ ^⊥ ∩ (b →₁c)^⊥ ^⊥ )) ∪ (0^⊥ ^⊥ ∩ (0 →₁c)^⊥ ^⊥ ))
50	23, 49	ax-r2 36	. . . 4 d = (((a^⊥ ^⊥ ∩ (a →₁c)^⊥ ^⊥ ) ∪ (b^⊥ ^⊥ ∩ (b →₁c)^⊥ ^⊥ )) ∪ (0^⊥ ^⊥ ∩ (0 →₁c)^⊥ ^⊥ ))
51		oa3-2lema 978	. . . . 5 ((a →₁d) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ 0) ∪ ((a →₁d) ∩ (0 →₁d))) ∩ ((b ∩ 0) ∪ ((b →₁d) ∩ (0 →₁d)))))))) = ((a →₁d) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))))))
52		oa3-2to2s.1	. . . . 5 ((a →₁d) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d)))))) ≤ d
53	51, 52	bltr 138	. . . 4 ((a →₁d) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ 0) ∪ ((a →₁d) ∩ (0 →₁d))) ∩ ((b ∩ 0) ∪ ((b →₁d) ∩ (0 →₁d)))))))) ≤ d
54	9, 15, 21, 50, 29, 36, 43, 53	oa4to6 965	. . 3 (((a^⊥ ∪ (a →₁c)^⊥ ) ∩ (b^⊥ ∪ (b →₁c)^⊥ )) ∩ (0^⊥ ∪ (0 →₁c)^⊥ )) ≤ ((a →₁c)^⊥ ∪ (a^⊥ ∩ (b^⊥ ∪ (((a^⊥ ∪ b^⊥ ) ∩ ((a →₁c)^⊥ ∪ (b →₁c)^⊥ )) ∩ (((a^⊥ ∪ 0^⊥ ) ∩ ((a →₁c)^⊥ ∪ (0 →₁c)^⊥ )) ∪ ((b^⊥ ∪ 0^⊥ ) ∩ ((b →₁c)^⊥ ∪ (0 →₁c)^⊥ )))))))
55	1, 2, 3, 54	oa6to4 958	. 2 ((a →₁c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c)))))))) ≤ (((a ∩ c) ∪ (b ∩ c)) ∪ (0 ∩ c))
56		oa3-2lema 978	. 2 ((a →₁c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c)))))))) = ((a →₁c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))))))
57		ancom 74	. . . . 5 (0 ∩ c) = (c ∩ 0)
58		an0 108	. . . . 5 (c ∩ 0) = 0
59	57, 58	ax-r2 36	. . . 4 (0 ∩ c) = 0
60	59	lor 70	. . 3 (((a ∩ c) ∪ (b ∩ c)) ∪ (0 ∩ c)) = (((a ∩ c) ∪ (b ∩ c)) ∪ 0)
61		or0 102	. . 3 (((a ∩ c) ∪ (b ∩ c)) ∪ 0) = ((a ∩ c) ∪ (b ∩ c))
62	60, 61	ax-r2 36	. 2 (((a ∩ c) ∪ (b ∩ c)) ∪ (0 ∩ c)) = ((a ∩ c) ∪ (b ∩ c))
63	55, 56, 62	le3tr2 141	1 ((a →₁c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))))) ≤ ((a ∩ c) ∪ (b ∩ c))

Colors of variables: term

Syntax hints: = wb 1 ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8 0wf 9 →₁wi1 12

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-i1 44 df-le1 130 df-le2 131 df-c1 132 df-c2 133

This theorem is referenced by: (None)

W3C validator