oa3-2lema - Quantum Logic Explorer

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

Theorem oa3-2lema 978

Description: Lemma for 3-OA(2). Equivalence with substitution into 4-OA. (Contributed by NM, 24-Dec-1998.)

**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 32	. . . . 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 108	. . . . . . . . . . 11 (a ∩ 0) = 0
3	2	ax-r5 38	. . . . . . . . . 10 ((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) = (0 ∪ ((a →₁c) ∩ (0 →₁c)))
4		ax-a2 31	. . . . . . . . . 10 (0 ∪ ((a →₁c) ∩ (0 →₁c))) = (((a →₁c) ∩ (0 →₁c)) ∪ 0)
5		or0 102	. . . . . . . . . . 11 (((a →₁c) ∩ (0 →₁c)) ∪ 0) = ((a →₁c) ∩ (0 →₁c))
6		0i1 273	. . . . . . . . . . . 12 (0 →₁c) = 1
7	6	lan 77	. . . . . . . . . . 11 ((a →₁c) ∩ (0 →₁c)) = ((a →₁c) ∩ 1)
8		an1 106	. . . . . . . . . . 11 ((a →₁c) ∩ 1) = (a →₁c)
9	5, 7, 8	3tr 65	. . . . . . . . . 10 (((a →₁c) ∩ (0 →₁c)) ∪ 0) = (a →₁c)
10	3, 4, 9	3tr 65	. . . . . . . . 9 ((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) = (a →₁c)
11		an0 108	. . . . . . . . . . 11 (b ∩ 0) = 0
12	11	ax-r5 38	. . . . . . . . . 10 ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))) = (0 ∪ ((b →₁c) ∩ (0 →₁c)))
13		ax-a2 31	. . . . . . . . . 10 (0 ∪ ((b →₁c) ∩ (0 →₁c))) = (((b →₁c) ∩ (0 →₁c)) ∪ 0)
14		or0 102	. . . . . . . . . . 11 (((b →₁c) ∩ (0 →₁c)) ∪ 0) = ((b →₁c) ∩ (0 →₁c))
15	6	lan 77	. . . . . . . . . . 11 ((b →₁c) ∩ (0 →₁c)) = ((b →₁c) ∩ 1)
16		an1 106	. . . . . . . . . . 11 ((b →₁c) ∩ 1) = (b →₁c)
17	14, 15, 16	3tr 65	. . . . . . . . . 10 (((b →₁c) ∩ (0 →₁c)) ∪ 0) = (b →₁c)
18	12, 13, 17	3tr 65	. . . . . . . . 9 ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))) = (b →₁c)
19	10, 18	2an 79	. . . . . . . 8 (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c)))) = ((a →₁c) ∩ (b →₁c))
20	19	lor 70	. . . . . . 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 110	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = ((a →₁c) ∩ (b →₁c))
22	20, 21	ax-r2 36	. . . . . 6 (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ 0) ∪ ((a →₁c) ∩ (0 →₁c))) ∩ ((b ∩ 0) ∪ ((b →₁c) ∩ (0 →₁c))))) = ((a →₁c) ∩ (b →₁c))
23	22	lor 70	. . . . 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 36	. . . 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 77	. . 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 70	. 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 77	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 8 0wf 9 →₁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

This theorem depends on definitions: df-a 40 df-t 41 df-f 42 df-i1 44

This theorem is referenced by: oa3-2to2s 990

W3C validator