oa3-u2lem - Quantum Logic Explorer

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

Theorem oa3-u2lem 986

Description: Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual. (Contributed by NM, 27-Dec-1998.)

**Assertion**
Ref	Expression
oa3-u2lem	((a →₁c) ∩ ((a^⊥ →₁c) ∪ (c ∩ ((((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) ∪ ((((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) ∩ ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c)))))))) = ((a →₁c) ∩ ((a^⊥ →₁c) ∪ (c ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))))))

**Proof of Theorem oa3-u2lem**
Step	Hyp	Ref	Expression
1		u1lemab 610	. . . . . . 7 ((a^⊥ →₁c) ∩ c) = ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c))
2		an1 106	. . . . . . 7 ((a →₁c) ∩ 1) = (a →₁c)
3	1, 2	2or 72	. . . . . 6 (((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) = (((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ∪ (a →₁c))
4		lea 160	. . . . . . . . 9 (a^⊥ ∩ c) ≤ a^⊥
5		ax-a1 30	. . . . . . . . . . . 12 a = a^⊥ ^⊥
6	5	ax-r1 35	. . . . . . . . . . 11 a^⊥ ^⊥ = a
7		leid 148	. . . . . . . . . . 11 a ≤ a
8	6, 7	bltr 138	. . . . . . . . . 10 a^⊥ ^⊥ ≤ a
9	8	leran 153	. . . . . . . . 9 (a^⊥ ^⊥ ∩ c) ≤ (a ∩ c)
10	4, 9	le2or 168	. . . . . . . 8 ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ≤ (a^⊥ ∪ (a ∩ c))
11		df-i1 44	. . . . . . . . 9 (a →₁c) = (a^⊥ ∪ (a ∩ c))
12	11	ax-r1 35	. . . . . . . 8 (a^⊥ ∪ (a ∩ c)) = (a →₁c)
13	10, 12	lbtr 139	. . . . . . 7 ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ≤ (a →₁c)
14	13	df-le2 131	. . . . . 6 (((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ∪ (a →₁c)) = (a →₁c)
15	3, 14	ax-r2 36	. . . . 5 (((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) = (a →₁c)
16		ancom 74	. . . . . 6 ((((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) ∩ ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c)))) = (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))))
17		ancom 74	. . . . . . . . . 10 (c ∩ (b^⊥ →₁c)) = ((b^⊥ →₁c) ∩ c)
18		u1lemab 610	. . . . . . . . . 10 ((b^⊥ →₁c) ∩ c) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
19	17, 18	ax-r2 36	. . . . . . . . 9 (c ∩ (b^⊥ →₁c)) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
20		ancom 74	. . . . . . . . . 10 (1 ∩ (b →₁c)) = ((b →₁c) ∩ 1)
21		an1 106	. . . . . . . . . 10 ((b →₁c) ∩ 1) = (b →₁c)
22	20, 21	ax-r2 36	. . . . . . . . 9 (1 ∩ (b →₁c)) = (b →₁c)
23	19, 22	2or 72	. . . . . . . 8 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ∪ (b →₁c))
24		lea 160	. . . . . . . . . . 11 (b^⊥ ∩ c) ≤ b^⊥
25		ax-a1 30	. . . . . . . . . . . . . 14 b = b^⊥ ^⊥
26	25	ax-r1 35	. . . . . . . . . . . . 13 b^⊥ ^⊥ = b
27		leid 148	. . . . . . . . . . . . 13 b ≤ b
28	26, 27	bltr 138	. . . . . . . . . . . 12 b^⊥ ^⊥ ≤ b
29	28	leran 153	. . . . . . . . . . 11 (b^⊥ ^⊥ ∩ c) ≤ (b ∩ c)
30	24, 29	le2or 168	. . . . . . . . . 10 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ≤ (b^⊥ ∪ (b ∩ c))
31		df-i1 44	. . . . . . . . . . 11 (b →₁c) = (b^⊥ ∪ (b ∩ c))
32	31	ax-r1 35	. . . . . . . . . 10 (b^⊥ ∪ (b ∩ c)) = (b →₁c)
33	30, 32	lbtr 139	. . . . . . . . 9 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ≤ (b →₁c)
34	33	df-le2 131	. . . . . . . 8 (((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ∪ (b →₁c)) = (b →₁c)
35	23, 34	ax-r2 36	. . . . . . 7 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (b →₁c)
36		ax-a2 31	. . . . . . 7 (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))
37	35, 36	2an 79	. . . . . 6 (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))) = ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))
38	16, 37	ax-r2 36	. . . . 5 ((((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) ∩ ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c)))) = ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))
39	15, 38	2or 72	. . . 4 ((((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) ∪ ((((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) ∩ ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))))) = ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))))
40	39	lan 77	. . 3 (c ∩ ((((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) ∪ ((((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) ∩ ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c)))))) = (c ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))))
41	40	lor 70	. 2 ((a^⊥ →₁c) ∪ (c ∩ ((((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) ∪ ((((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) ∩ ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))))))) = ((a^⊥ →₁c) ∪ (c ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))))))
42	41	lan 77	1 ((a →₁c) ∩ ((a^⊥ →₁c) ∪ (c ∩ ((((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) ∪ ((((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) ∩ ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c)))))))) = ((a →₁c) ∩ ((a^⊥ →₁c) ∪ (c ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))))))

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8 →₁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: oa3-u2 992

W3C validator