Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa3-u2lem 966

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

**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 592	. . . . . . 7 ((a^⊥ →₁c) ∩ c) = ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c))
2		an1 98	. . . . . . 7 ((a →₁c) ∩ 1) = (a →₁c)
3	1, 2	2or 67	. . . . . 6 (((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) = (((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ∪ (a →₁c))
4		lea 152	. . . . . . . . 9 (a^⊥ ∩ c) ≤ a^⊥
5		ax-a1 29	. . . . . . . . . . . 12 a = a^⊥ ^⊥
6	5	ax-r1 34	. . . . . . . . . . 11 a^⊥ ^⊥ = a
7		leid 140	. . . . . . . . . . 11 a ≤ a
8	6, 7	bltr 130	. . . . . . . . . 10 a^⊥ ^⊥ ≤ a
9	8	leran 145	. . . . . . . . 9 (a^⊥ ^⊥ ∩ c) ≤ (a ∩ c)
10	4, 9	le2or 160	. . . . . . . 8 ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ≤ (a^⊥ ∪ (a ∩ c))
11		df-i1 43	. . . . . . . . 9 (a →₁c) = (a^⊥ ∪ (a ∩ c))
12	11	ax-r1 34	. . . . . . . 8 (a^⊥ ∪ (a ∩ c)) = (a →₁c)
13	10, 12	lbtr 131	. . . . . . 7 ((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ≤ (a →₁c)
14	13	df-le2 123	. . . . . 6 (((a^⊥ ∩ c) ∪ (a^⊥ ^⊥ ∩ c)) ∪ (a →₁c)) = (a →₁c)
15	3, 14	ax-r2 35	. . . . 5 (((a^⊥ →₁c) ∩ c) ∪ ((a →₁c) ∩ 1)) = (a →₁c)
16		ancom 68	. . . . . 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 68	. . . . . . . . . 10 (c ∩ (b^⊥ →₁c)) = ((b^⊥ →₁c) ∩ c)
18		u1lemab 592	. . . . . . . . . 10 ((b^⊥ →₁c) ∩ c) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
19	17, 18	ax-r2 35	. . . . . . . . 9 (c ∩ (b^⊥ →₁c)) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
20		ancom 68	. . . . . . . . . 10 (1 ∩ (b →₁c)) = ((b →₁c) ∩ 1)
21		an1 98	. . . . . . . . . 10 ((b →₁c) ∩ 1) = (b →₁c)
22	20, 21	ax-r2 35	. . . . . . . . 9 (1 ∩ (b →₁c)) = (b →₁c)
23	19, 22	2or 67	. . . . . . . 8 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ∪ (b →₁c))
24		lea 152	. . . . . . . . . . 11 (b^⊥ ∩ c) ≤ b^⊥
25		ax-a1 29	. . . . . . . . . . . . . 14 b = b^⊥ ^⊥
26	25	ax-r1 34	. . . . . . . . . . . . 13 b^⊥ ^⊥ = b
27		leid 140	. . . . . . . . . . . . 13 b ≤ b
28	26, 27	bltr 130	. . . . . . . . . . . 12 b^⊥ ^⊥ ≤ b
29	28	leran 145	. . . . . . . . . . 11 (b^⊥ ^⊥ ∩ c) ≤ (b ∩ c)
30	24, 29	le2or 160	. . . . . . . . . 10 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ≤ (b^⊥ ∪ (b ∩ c))
31		df-i1 43	. . . . . . . . . . 11 (b →₁c) = (b^⊥ ∪ (b ∩ c))
32	31	ax-r1 34	. . . . . . . . . 10 (b^⊥ ∪ (b ∩ c)) = (b →₁c)
33	30, 32	lbtr 131	. . . . . . . . 9 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ≤ (b →₁c)
34	33	df-le2 123	. . . . . . . 8 (((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ∪ (b →₁c)) = (b →₁c)
35	23, 34	ax-r2 35	. . . . . . 7 ((c ∩ (b^⊥ →₁c)) ∪ (1 ∩ (b →₁c))) = (b →₁c)
36		ax-a2 30	. . . . . . 7 (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a^⊥ →₁c) ∩ (b^⊥ →₁c)))
37	35, 36	2an 72	. . . . . 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 35	. . . . 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 67	. . . 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 70	. . 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 66	. 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 70	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 9 →₁wi1 13

This theorem is referenced by: oa3-u2 972

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