oa3-u1 - Quantum Logic Explorer

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

Theorem oa3-u1 991

Description: Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA. (Contributed by NM, 27-Dec-1998.)

**Hypothesis**
Ref	Expression
oa3-u1.1	((c →₁c) ∩ (c ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ ((c →₁c) ∩ ((a^⊥ →₁c) →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ ((c →₁c) ∩ ((b^⊥ →₁c) →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ (((a^⊥ →₁c) →₁c) ∩ ((b^⊥ →₁c) →₁c)))))))) ≤ c

**Assertion**
Ref	Expression
oa3-u1	(c ∪ ((a^⊥ →₁c) ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))))) ≤ c

**Proof of Theorem oa3-u1**
Step	Hyp	Ref	Expression
1		oa3-u1lem 985	. . 3 (1 ∩ (c ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))))))) = (c ∪ ((a^⊥ →₁c) ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))))))
2	1	ax-r1 35	. 2 (c ∪ ((a^⊥ →₁c) ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))))) = (1 ∩ (c ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))))))))
3		le1 146	. . . 4 c^⊥ ≤ 1
4		u1lem9ab 779	. . . 4 (a^⊥ →₁c)^⊥ ≤ (a →₁c)
5		u1lem9ab 779	. . . 4 (b^⊥ →₁c)^⊥ ≤ (b →₁c)
6		ax-a2 31	. . . . . . 7 (c ∪ ((b ∩ c) ∪ (b^⊥ ∩ c))) = (((b ∩ c) ∪ (b^⊥ ∩ c)) ∪ c)
7		lear 161	. . . . . . . . 9 (b ∩ c) ≤ c
8		lear 161	. . . . . . . . 9 (b^⊥ ∩ c) ≤ c
9	7, 8	lel2or 170	. . . . . . . 8 ((b ∩ c) ∪ (b^⊥ ∩ c)) ≤ c
10	9	df-le2 131	. . . . . . 7 (((b ∩ c) ∪ (b^⊥ ∩ c)) ∪ c) = c
11	6, 10	ax-r2 36	. . . . . 6 (c ∪ ((b ∩ c) ∪ (b^⊥ ∩ c))) = c
12	11	ax-r1 35	. . . . 5 c = (c ∪ ((b ∩ c) ∪ (b^⊥ ∩ c)))
13		an1 106	. . . . . . . . 9 (c ∩ 1) = c
14		ancom 74	. . . . . . . . . 10 ((a^⊥ →₁c) ∩ (a →₁c)) = ((a →₁c) ∩ (a^⊥ →₁c))
15		u1lem8 776	. . . . . . . . . 10 ((a →₁c) ∩ (a^⊥ →₁c)) = ((a ∩ c) ∪ (a^⊥ ∩ c))
16	14, 15	ax-r2 36	. . . . . . . . 9 ((a^⊥ →₁c) ∩ (a →₁c)) = ((a ∩ c) ∪ (a^⊥ ∩ c))
17	13, 16	2or 72	. . . . . . . 8 ((c ∩ 1) ∪ ((a^⊥ →₁c) ∩ (a →₁c))) = (c ∪ ((a ∩ c) ∪ (a^⊥ ∩ c)))
18		ax-a2 31	. . . . . . . 8 (c ∪ ((a ∩ c) ∪ (a^⊥ ∩ c))) = (((a ∩ c) ∪ (a^⊥ ∩ c)) ∪ c)
19		lear 161	. . . . . . . . . 10 (a ∩ c) ≤ c
20		lear 161	. . . . . . . . . 10 (a^⊥ ∩ c) ≤ c
21	19, 20	lel2or 170	. . . . . . . . 9 ((a ∩ c) ∪ (a^⊥ ∩ c)) ≤ c
22	21	df-le2 131	. . . . . . . 8 (((a ∩ c) ∪ (a^⊥ ∩ c)) ∪ c) = c
23	17, 18, 22	3tr 65	. . . . . . 7 ((c ∩ 1) ∪ ((a^⊥ →₁c) ∩ (a →₁c))) = c
24		ancom 74	. . . . . . . 8 ((b^⊥ →₁c) ∩ (b →₁c)) = ((b →₁c) ∩ (b^⊥ →₁c))
25		u1lem8 776	. . . . . . . 8 ((b →₁c) ∩ (b^⊥ →₁c)) = ((b ∩ c) ∪ (b^⊥ ∩ c))
26	24, 25	ax-r2 36	. . . . . . 7 ((b^⊥ →₁c) ∩ (b →₁c)) = ((b ∩ c) ∪ (b^⊥ ∩ c))
27	23, 26	2or 72	. . . . . 6 (((c ∩ 1) ∪ ((a^⊥ →₁c) ∩ (a →₁c))) ∪ ((b^⊥ →₁c) ∩ (b →₁c))) = (c ∪ ((b ∩ c) ∪ (b^⊥ ∩ c)))
28	27	ax-r1 35	. . . . 5 (c ∪ ((b ∩ c) ∪ (b^⊥ ∩ c))) = (((c ∩ 1) ∪ ((a^⊥ →₁c) ∩ (a →₁c))) ∪ ((b^⊥ →₁c) ∩ (b →₁c)))
29	12, 28	ax-r2 36	. . . 4 c = (((c ∩ 1) ∪ ((a^⊥ →₁c) ∩ (a →₁c))) ∪ ((b^⊥ →₁c) ∩ (b →₁c)))
30		oa3-u1.1	. . . 4 ((c →₁c) ∩ (c ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ ((c →₁c) ∩ ((a^⊥ →₁c) →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ ((c →₁c) ∩ ((b^⊥ →₁c) →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ (((a^⊥ →₁c) →₁c) ∩ ((b^⊥ →₁c) →₁c)))))))) ≤ c
31	3, 4, 5, 29, 30	oa4to6dual 964	. . 3 (1 ∩ (c ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))))))) ≤ c
32		leid 148	. . 3 c ≤ c
33	31, 32	letr 137	. 2 (1 ∩ (c ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))))))) ≤ c
34	2, 33	bltr 138	1 (c ∪ ((a^⊥ →₁c) ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))))) ≤ c

Colors of variables: term

This proof depends on syntax axioms: ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8 →₁wi1 12

This proof depends on 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 proof 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 used by: (None)

W3C validator