Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa3-u1lem 965

Description: Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual.

**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 68	. 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 98	. 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 152	. . . . . . . . 9 (a^⊥ ∩ c) ≤ a^⊥
4		leo 150	. . . . . . . . 9 a^⊥ ≤ (a^⊥ ∪ (a ∩ c))
5	3, 4	letr 129	. . . . . . . 8 (a^⊥ ∩ c) ≤ (a^⊥ ∪ (a ∩ c))
6		leor 151	. . . . . . . 8 (a ∩ c) ≤ (a^⊥ ∪ (a ∩ c))
7	5, 6	lel2or 162	. . . . . . 7 ((a^⊥ ∩ c) ∪ (a ∩ c)) ≤ (a^⊥ ∪ (a ∩ c))
8	7	df-le2 123	. . . . . 6 (((a^⊥ ∩ c) ∪ (a ∩ c)) ∪ (a^⊥ ∪ (a ∩ c))) = (a^⊥ ∪ (a ∩ c))
9		ancom 68	. . . . . . . 8 (c ∩ (a^⊥ →₁c)) = ((a^⊥ →₁c) ∩ c)
10		u1lemab 592	. . . . . . . 8 ((a^⊥ →₁c) ∩ c) = ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c))
11		ax-a1 29	. . . . . . . . . . 11 a = a^⊥ ^⊥
12	11	ax-r1 34	. . . . . . . . . 10 a^⊥ ^⊥ = a
13	12	ran 71	. . . . . . . . 9 (a^⊥ ^⊥ ∩ c) = (a ∩ c)
14	13	lor 66	. . . . . . . 8 ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) = ((a^⊥ ∩ c) ∪ (a ∩ c))
15	9, 10, 14	3tr 62	. . . . . . 7 (c ∩ (a^⊥ →₁c)) = ((a^⊥ ∩ c) ∪ (a ∩ c))
16		ancom 68	. . . . . . . 8 (1 ∩ (a →₁c)) = ((a →₁c) ∩ 1)
17		an1 98	. . . . . . . 8 ((a →₁c) ∩ 1) = (a →₁c)
18		df-i1 43	. . . . . . . 8 (a →₁c) = (a^⊥ ∪ (a ∩ c))
19	16, 17, 18	3tr 62	. . . . . . 7 (1 ∩ (a →₁c)) = (a^⊥ ∪ (a ∩ c))
20	15, 19	2or 67	. . . . . 6 ((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) = (((a^⊥ ∩ c) ∪ (a ∩ c)) ∪ (a^⊥ ∪ (a ∩ c)))
21	8, 20, 18	3tr1 60	. . . . 5 ((c ∩ (a^⊥ →₁c)) ∪ (1 ∩ (a →₁c))) = (a →₁c)
22		lea 152	. . . . . . . . . 10 (b^⊥ ∩ c) ≤ b^⊥
23		leo 150	. . . . . . . . . 10 b^⊥ ≤ (b^⊥ ∪ (b ∩ c))
24	22, 23	letr 129	. . . . . . . . 9 (b^⊥ ∩ c) ≤ (b^⊥ ∪ (b ∩ c))
25		leor 151	. . . . . . . . 9 (b ∩ c) ≤ (b^⊥ ∪ (b ∩ c))
26	24, 25	lel2or 162	. . . . . . . 8 ((b^⊥ ∩ c) ∪ (b ∩ c)) ≤ (b^⊥ ∪ (b ∩ c))
27	26	df-le2 123	. . . . . . 7 (((b^⊥ ∩ c) ∪ (b ∩ c)) ∪ (b^⊥ ∪ (b ∩ c))) = (b^⊥ ∪ (b ∩ c))
28		ancom 68	. . . . . . . . 9 (c ∩ (b^⊥ →₁c)) = ((b^⊥ →₁c) ∩ c)
29		u1lemab 592	. . . . . . . . 9 ((b^⊥ →₁c) ∩ c) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
30		ax-a1 29	. . . . . . . . . . . 12 b = b^⊥ ^⊥
31	30	ax-r1 34	. . . . . . . . . . 11 b^⊥ ^⊥ = b
32	31	ran 71	. . . . . . . . . 10 (b^⊥ ^⊥ ∩ c) = (b ∩ c)
33	32	lor 66	. . . . . . . . 9 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) = ((b^⊥ ∩ c) ∪ (b ∩ c))
34	28, 29, 33	3tr 62	. . . . . . . 8 (c ∩ (b^⊥ →₁c)) = ((b^⊥ ∩ c) ∪ (b ∩ c))
35		ancom 68	. . . . . . . . 9 (1 ∩ (b →₁c)) = ((b →₁c) ∩ 1)
36		an1 98	. . . . . . . . 9 ((b →₁c) ∩ 1) = (b →₁c)
37		df-i1 43	. . . . . . . . 9 (b →₁c) = (b^⊥ ∪ (b ∩ c))
38	35, 36, 37	3tr 62	. . . . . . . 8 (1 ∩ (b →₁c)) = (b^⊥ ∪ (b ∩ c))
39	34, 38	2or 67	. . . . . . 7 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (((b^⊥ ∩ c) ∪ (b ∩ c)) ∪ (b^⊥ ∪ (b ∩ c)))
40	27, 39, 37	3tr1 60	. . . . . 6 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (b →₁c)
41		ax-a2 30	. . . . . 6 (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))
42	40, 41	2an 72	. . . . 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 67	. . . 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 70	. . 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 66	. 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 62	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 9 →₁wi1 13

This theorem is referenced by: oa3-u1 971

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

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i1 43 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org