Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa3-2lema 958

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

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

**Proof of Theorem oa3-2lema**
Step	Hyp	Ref	Expression
1		ax-a3 31	. . . . 5 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))))) = ((a ∩ b) ∪ (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))))))
2		an0 100	. . . . . . . . . . 11 (a ∩ 0) = 0
3	2	ax-r5 37	. . . . . . . . . 10 ((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) = (0 ∪ ((a →₁c) ∩ (0 →₁c)))
4		ax-a2 30	. . . . . . . . . 10 (0 ∪ ((a →₁c) ∩ (0 →₁c))) = (((a →₁c) ∩ (0 →₁c)) ∪ 0)
5		or0 94	. . . . . . . . . . 11 (((a →₁c) ∩ (0 →₁c)) ∪ 0) = ((a →₁c) ∩ (0 →₁c))
6		0i1 265	. . . . . . . . . . . 12 (0 →₁c) = 1
7	6	lan 70	. . . . . . . . . . 11 ((a →₁c) ∩ (0 →₁c)) = ((a →₁c) ∩ 1)
8		an1 98	. . . . . . . . . . 11 ((a →₁c) ∩ 1) = (a →₁c)
9	5, 7, 8	3tr 62	. . . . . . . . . 10 (((a →₁c) ∩ (0 →₁c)) ∪ 0) = (a →₁c)
10	3, 4, 9	3tr 62	. . . . . . . . 9 ((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) = (a →₁c)
11		an0 100	. . . . . . . . . . 11 (b ∩ 0) = 0
12	11	ax-r5 37	. . . . . . . . . 10 ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))) = (0 ∪ ((b →₁c) ∩ (0 →₁c)))
13		ax-a2 30	. . . . . . . . . 10 (0 ∪ ((b →₁c) ∩ (0 →₁c))) = (((b →₁c) ∩ (0 →₁c)) ∪ 0)
14		or0 94	. . . . . . . . . . 11 (((b →₁c) ∩ (0 →₁c)) ∪ 0) = ((b →₁c) ∩ (0 →₁c))
15	6	lan 70	. . . . . . . . . . 11 ((b →₁c) ∩ (0 →₁c)) = ((b →₁c) ∩ 1)
16		an1 98	. . . . . . . . . . 11 ((b →₁c) ∩ 1) = (b →₁c)
17	14, 15, 16	3tr 62	. . . . . . . . . 10 (((b →₁c) ∩ (0 →₁c)) ∪ 0) = (b →₁c)
18	12, 13, 17	3tr 62	. . . . . . . . 9 ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))) = (b →₁c)
19	10, 18	2an 72	. . . . . . . 8 (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c)))) = ((a →₁c) ∩ (b →₁c))
20	19	lor 66	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))
21		oridm 102	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = ((a →₁c) ∩ (b →₁c))
22	20, 21	ax-r2 35	. . . . . 6 (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))))) = ((a →₁c) ∩ (b →₁c))
23	22	lor 66	. . . . 5 ((a ∩ b) ∪ (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c)))))) = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
24	1, 23	ax-r2 35	. . . 4 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))))) = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
25	24	lan 70	. . 3 (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c)))))) = (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))))
26	25	lor 66	. 2 (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))))))) = (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))))
27	26	lan 70	1 ((a →₁c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c)))))))) = ((a →₁c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))))))

Colors of variables: term

Syntax hints: = wb 1 ∪ wo 6 ∩ wa 7 1wt 9 0wf 10 →₁wi1 13

This theorem is referenced by: oa3-2to2s 970

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

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

metamath.org