Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa3-2lemb 959

Description: Lemma for 3-OA(2). Equivalence with substitution into 4-OA.

**Assertion**
Ref	Expression
oa3-2lemb	((a →₁c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c)))))))) = ((a →₁c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))))))

**Proof of Theorem oa3-2lemb**
Step	Hyp	Ref	Expression
1		ax-a3 31	. . . . 5 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))))) = ((a ∩ b) ∪ (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))))))
2		i1id 267	. . . . . . . . . . . . 13 (c →₁c) = 1
3	2	lan 70	. . . . . . . . . . . 12 ((a →₁c) ∩ (c →₁c)) = ((a →₁c) ∩ 1)
4		an1 98	. . . . . . . . . . . 12 ((a →₁c) ∩ 1) = (a →₁c)
5	3, 4	ax-r2 35	. . . . . . . . . . 11 ((a →₁c) ∩ (c →₁c)) = (a →₁c)
6	5	lor 66	. . . . . . . . . 10 ((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) = ((a ∩ c) ∪ (a →₁c))
7		or12 73	. . . . . . . . . . . 12 ((a ∩ c) ∪ (a^⊥ ∪ (a ∩ c))) = (a^⊥ ∪ ((a ∩ c) ∪ (a ∩ c)))
8		oridm 102	. . . . . . . . . . . . 13 ((a ∩ c) ∪ (a ∩ c)) = (a ∩ c)
9	8	lor 66	. . . . . . . . . . . 12 (a^⊥ ∪ ((a ∩ c) ∪ (a ∩ c))) = (a^⊥ ∪ (a ∩ c))
10	7, 9	ax-r2 35	. . . . . . . . . . 11 ((a ∩ c) ∪ (a^⊥ ∪ (a ∩ c))) = (a^⊥ ∪ (a ∩ c))
11		df-i1 43	. . . . . . . . . . . 12 (a →₁c) = (a^⊥ ∪ (a ∩ c))
12	11	lor 66	. . . . . . . . . . 11 ((a ∩ c) ∪ (a →₁c)) = ((a ∩ c) ∪ (a^⊥ ∪ (a ∩ c)))
13	10, 12, 11	3tr1 60	. . . . . . . . . 10 ((a ∩ c) ∪ (a →₁c)) = (a →₁c)
14	6, 13	ax-r2 35	. . . . . . . . 9 ((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) = (a →₁c)
15	2	lan 70	. . . . . . . . . . . 12 ((b →₁c) ∩ (c →₁c)) = ((b →₁c) ∩ 1)
16		an1 98	. . . . . . . . . . . 12 ((b →₁c) ∩ 1) = (b →₁c)
17	15, 16	ax-r2 35	. . . . . . . . . . 11 ((b →₁c) ∩ (c →₁c)) = (b →₁c)
18	17	lor 66	. . . . . . . . . 10 ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))) = ((b ∩ c) ∪ (b →₁c))
19		or12 73	. . . . . . . . . . . 12 ((b ∩ c) ∪ (b^⊥ ∪ (b ∩ c))) = (b^⊥ ∪ ((b ∩ c) ∪ (b ∩ c)))
20		oridm 102	. . . . . . . . . . . . 13 ((b ∩ c) ∪ (b ∩ c)) = (b ∩ c)
21	20	lor 66	. . . . . . . . . . . 12 (b^⊥ ∪ ((b ∩ c) ∪ (b ∩ c))) = (b^⊥ ∪ (b ∩ c))
22	19, 21	ax-r2 35	. . . . . . . . . . 11 ((b ∩ c) ∪ (b^⊥ ∪ (b ∩ c))) = (b^⊥ ∪ (b ∩ c))
23		df-i1 43	. . . . . . . . . . . 12 (b →₁c) = (b^⊥ ∪ (b ∩ c))
24	23	lor 66	. . . . . . . . . . 11 ((b ∩ c) ∪ (b →₁c)) = ((b ∩ c) ∪ (b^⊥ ∪ (b ∩ c)))
25	22, 24, 23	3tr1 60	. . . . . . . . . 10 ((b ∩ c) ∪ (b →₁c)) = (b →₁c)
26	18, 25	ax-r2 35	. . . . . . . . 9 ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))) = (b →₁c)
27	14, 26	2an 72	. . . . . . . 8 (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c)))) = ((a →₁c) ∩ (b →₁c))
28	27	lor 66	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))
29		oridm 102	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = ((a →₁c) ∩ (b →₁c))
30	28, 29	ax-r2 35	. . . . . 6 (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))))) = ((a →₁c) ∩ (b →₁c))
31	30	lor 66	. . . . 5 ((a ∩ b) ∪ (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c)))))) = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
32	1, 31	ax-r2 35	. . . 4 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))))) = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
33	32	lan 70	. . 3 (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c)))))) = (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))))
34	33	lor 66	. 2 (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))))))) = (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))))
35	34	lan 70	1 ((a →₁c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c)))))))) = ((a →₁c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((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-2to4 968

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

This theorem depends on definitions: df-a 39 df-t 40 df-f 41 df-i1 43

metamath.org