oa3-2lemb - Quantum Logic Explorer

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

Theorem oa3-2lemb 979

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

**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 32	. . . . 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 275	. . . . . . . . . . . . 13 (c →₁c) = 1
3	2	lan 77	. . . . . . . . . . . 12 ((a →₁c) ∩ (c →₁c)) = ((a →₁c) ∩ 1)
4		an1 106	. . . . . . . . . . . 12 ((a →₁c) ∩ 1) = (a →₁c)
5	3, 4	ax-r2 36	. . . . . . . . . . 11 ((a →₁c) ∩ (c →₁c)) = (a →₁c)
6	5	lor 70	. . . . . . . . . 10 ((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) = ((a ∩ c) ∪ (a →₁c))
7		or12 80	. . . . . . . . . . . 12 ((a ∩ c) ∪ (a^⊥ ∪ (a ∩ c))) = (a^⊥ ∪ ((a ∩ c) ∪ (a ∩ c)))
8		oridm 110	. . . . . . . . . . . . 13 ((a ∩ c) ∪ (a ∩ c)) = (a ∩ c)
9	8	lor 70	. . . . . . . . . . . 12 (a^⊥ ∪ ((a ∩ c) ∪ (a ∩ c))) = (a^⊥ ∪ (a ∩ c))
10	7, 9	ax-r2 36	. . . . . . . . . . 11 ((a ∩ c) ∪ (a^⊥ ∪ (a ∩ c))) = (a^⊥ ∪ (a ∩ c))
11		df-i1 44	. . . . . . . . . . . 12 (a →₁c) = (a^⊥ ∪ (a ∩ c))
12	11	lor 70	. . . . . . . . . . 11 ((a ∩ c) ∪ (a →₁c)) = ((a ∩ c) ∪ (a^⊥ ∪ (a ∩ c)))
13	10, 12, 11	3tr1 63	. . . . . . . . . 10 ((a ∩ c) ∪ (a →₁c)) = (a →₁c)
14	6, 13	ax-r2 36	. . . . . . . . 9 ((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) = (a →₁c)
15	2	lan 77	. . . . . . . . . . . 12 ((b →₁c) ∩ (c →₁c)) = ((b →₁c) ∩ 1)
16		an1 106	. . . . . . . . . . . 12 ((b →₁c) ∩ 1) = (b →₁c)
17	15, 16	ax-r2 36	. . . . . . . . . . 11 ((b →₁c) ∩ (c →₁c)) = (b →₁c)
18	17	lor 70	. . . . . . . . . 10 ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))) = ((b ∩ c) ∪ (b →₁c))
19		or12 80	. . . . . . . . . . . 12 ((b ∩ c) ∪ (b^⊥ ∪ (b ∩ c))) = (b^⊥ ∪ ((b ∩ c) ∪ (b ∩ c)))
20		oridm 110	. . . . . . . . . . . . 13 ((b ∩ c) ∪ (b ∩ c)) = (b ∩ c)
21	20	lor 70	. . . . . . . . . . . 12 (b^⊥ ∪ ((b ∩ c) ∪ (b ∩ c))) = (b^⊥ ∪ (b ∩ c))
22	19, 21	ax-r2 36	. . . . . . . . . . 11 ((b ∩ c) ∪ (b^⊥ ∪ (b ∩ c))) = (b^⊥ ∪ (b ∩ c))
23		df-i1 44	. . . . . . . . . . . 12 (b →₁c) = (b^⊥ ∪ (b ∩ c))
24	23	lor 70	. . . . . . . . . . 11 ((b ∩ c) ∪ (b →₁c)) = ((b ∩ c) ∪ (b^⊥ ∪ (b ∩ c)))
25	22, 24, 23	3tr1 63	. . . . . . . . . 10 ((b ∩ c) ∪ (b →₁c)) = (b →₁c)
26	18, 25	ax-r2 36	. . . . . . . . 9 ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))) = (b →₁c)
27	14, 26	2an 79	. . . . . . . 8 (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c)))) = ((a →₁c) ∩ (b →₁c))
28	27	lor 70	. . . . . . 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 110	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = ((a →₁c) ∩ (b →₁c))
30	28, 29	ax-r2 36	. . . . . 6 (((a →₁c) ∩ (b →₁c)) ∪ (((a ∩ c) ∪ ((a →₁c) ∩ (c →₁c))) ∩ ((b ∩ c) ∪ ((b →₁c) ∩ (c →₁c))))) = ((a →₁c) ∩ (b →₁c))
31	30	lor 70	. . . . 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 36	. . . 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 77	. . 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 70	. 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 77	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

This proof depends on syntax axioms: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8 →₁wi1 12

This proof depends on axioms: ax-a1 30 ax-a2 31 ax-a3 32 ax-a5 34 ax-r1 35 ax-r2 36 ax-r4 37 ax-r5 38

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

This theorem is used by: oa3-2to4 988

W3C validator