oa3-u1lem - Quantum Logic Explorer

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

Theorem oa3-u1lem 985

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

**Assertion**
Ref	Expression
oa3-u1lem	(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)))))))

**Proof of Theorem oa3-u1lem**
Step	Hyp	Ref	Expression
1		ancom 74	. 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 ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))))))) ∩ 1)
2		an1 106	. 2 ((c ∪ ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (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		lea 160	. . . . . . . . 9 (a^⊥ ∩ c) ≤ a^⊥
4		leo 158	. . . . . . . . 9 a^⊥ ≤ (a^⊥ ∪ (a ∩ c))
5	3, 4	letr 137	. . . . . . . 8 (a^⊥ ∩ c) ≤ (a^⊥ ∪ (a ∩ c))
6		leor 159	. . . . . . . 8 (a ∩ c) ≤ (a^⊥ ∪ (a ∩ c))
7	5, 6	lel2or 170	. . . . . . 7 ((a^⊥ ∩ c) ∪ (a ∩ c)) ≤ (a^⊥ ∪ (a ∩ c))
8	7	df-le2 131	. . . . . 6 (((a^⊥ ∩ c) ∪ (a ∩ c)) ∪ (a^⊥ ∪ (a ∩ c))) = (a^⊥ ∪ (a ∩ c))
9		ancom 74	. . . . . . . 8 (c ∩ (a^⊥ →₁c)) = ((a^⊥ →₁c) ∩ c)
10		u1lemab 610	. . . . . . . 8 ((a^⊥ →₁c) ∩ c) = ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c))
11		ax-a1 30	. . . . . . . . . . 11 a = a^⊥ ^⊥
12	11	ax-r1 35	. . . . . . . . . 10 a^⊥ ^⊥ = a
13	12	ran 78	. . . . . . . . 9 (a^⊥ ^⊥ ∩ c) = (a ∩ c)
14	13	lor 70	. . . . . . . 8 ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) = ((a^⊥ ∩ c) ∪ (a ∩ c))
15	9, 10, 14	3tr 65	. . . . . . 7 (c ∩ (a^⊥ →₁c)) = ((a^⊥ ∩ c) ∪ (a ∩ c))
16		ancom 74	. . . . . . . 8 (1 ∩ (a →₁c)) = ((a →₁c) ∩ 1)
17		an1 106	. . . . . . . 8 ((a →₁c) ∩ 1) = (a →₁c)
18		df-i1 44	. . . . . . . 8 (a →₁c) = (a^⊥ ∪ (a ∩ c))
19	16, 17, 18	3tr 65	. . . . . . 7 (1 ∩ (a →₁c)) = (a^⊥ ∪ (a ∩ c))
20	15, 19	2or 72	. . . . . 6 ((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) = (((a^⊥ ∩ c) ∪ (a ∩ c)) ∪ (a^⊥ ∪ (a ∩ c)))
21	8, 20, 18	3tr1 63	. . . . 5 ((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) = (a →₁c)
22		lea 160	. . . . . . . . . 10 (b^⊥ ∩ c) ≤ b^⊥
23		leo 158	. . . . . . . . . 10 b^⊥ ≤ (b^⊥ ∪ (b ∩ c))
24	22, 23	letr 137	. . . . . . . . 9 (b^⊥ ∩ c) ≤ (b^⊥ ∪ (b ∩ c))
25		leor 159	. . . . . . . . 9 (b ∩ c) ≤ (b^⊥ ∪ (b ∩ c))
26	24, 25	lel2or 170	. . . . . . . 8 ((b^⊥ ∩ c) ∪ (b ∩ c)) ≤ (b^⊥ ∪ (b ∩ c))
27	26	df-le2 131	. . . . . . 7 (((b^⊥ ∩ c) ∪ (b ∩ c)) ∪ (b^⊥ ∪ (b ∩ c))) = (b^⊥ ∪ (b ∩ c))
28		ancom 74	. . . . . . . . 9 (c ∩ (b^⊥ →₁c)) = ((b^⊥ →₁c) ∩ c)
29		u1lemab 610	. . . . . . . . 9 ((b^⊥ →₁c) ∩ c) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
30		ax-a1 30	. . . . . . . . . . . 12 b = b^⊥ ^⊥
31	30	ax-r1 35	. . . . . . . . . . 11 b^⊥ ^⊥ = b
32	31	ran 78	. . . . . . . . . 10 (b^⊥ ^⊥ ∩ c) = (b ∩ c)
33	32	lor 70	. . . . . . . . 9 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) = ((b^⊥ ∩ c) ∪ (b ∩ c))
34	28, 29, 33	3tr 65	. . . . . . . 8 (c ∩ (b^⊥ →₁c)) = ((b^⊥ ∩ c) ∪ (b ∩ c))
35		ancom 74	. . . . . . . . 9 (1 ∩ (b →₁c)) = ((b →₁c) ∩ 1)
36		an1 106	. . . . . . . . 9 ((b →₁c) ∩ 1) = (b →₁c)
37		df-i1 44	. . . . . . . . 9 (b →₁c) = (b^⊥ ∪ (b ∩ c))
38	35, 36, 37	3tr 65	. . . . . . . 8 (1 ∩ (b →₁c)) = (b^⊥ ∪ (b ∩ c))
39	34, 38	2or 72	. . . . . . 7 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (((b^⊥ ∩ c) ∪ (b ∩ c)) ∪ (b^⊥ ∪ (b ∩ c)))
40	27, 39, 37	3tr1 63	. . . . . 6 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (b →₁c)
41		ax-a2 31	. . . . . 6 (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))
42	40, 41	2an 79	. . . . 5 (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))) = ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))
43	21, 42	2or 72	. . . 4 (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))))
44	43	lan 77	. . 3 ((a^⊥ →₁c) ∩ (((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) ∪ (((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))))) = ((a^⊥ →₁c) ∩ ((a →₁c) ∪ ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c))))))
45	44	lor 70	. 2 (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)))))))
46	1, 2, 45	3tr 65	1 (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)))))))

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-u1 991

W3C validator