oa3-6lem - Quantum Logic Explorer

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

Theorem oa3-6lem 980

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

**Assertion**
Ref	Expression
oa3-6lem	((a →₁c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) ∩ ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c)))))))) = ((a →₁c) ∩ (a ∪ (b ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))))))

**Proof of Theorem oa3-6lem**
Step	Hyp	Ref	Expression
1		an1 106	. . . . . . . . 9 (a ∩ 1) = a
2		1i1 274	. . . . . . . . . . 11 (1 →₁c) = c
3	2	lan 77	. . . . . . . . . 10 ((a →₁c) ∩ (1 →₁c)) = ((a →₁c) ∩ c)
4		u1lemab 610	. . . . . . . . . 10 ((a →₁c) ∩ c) = ((a ∩ c) ∪ (a^⊥ ∩ c))
5	3, 4	ax-r2 36	. . . . . . . . 9 ((a →₁c) ∩ (1 →₁c)) = ((a ∩ c) ∪ (a^⊥ ∩ c))
6	1, 5	2or 72	. . . . . . . 8 ((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) = (a ∪ ((a ∩ c) ∪ (a^⊥ ∩ c)))
7		ax-a3 32	. . . . . . . . 9 ((a ∪ (a ∩ c)) ∪ (a^⊥ ∩ c)) = (a ∪ ((a ∩ c) ∪ (a^⊥ ∩ c)))
8	7	ax-r1 35	. . . . . . . 8 (a ∪ ((a ∩ c) ∪ (a^⊥ ∩ c))) = ((a ∪ (a ∩ c)) ∪ (a^⊥ ∩ c))
9		orabs 120	. . . . . . . . 9 (a ∪ (a ∩ c)) = a
10	9	ax-r5 38	. . . . . . . 8 ((a ∪ (a ∩ c)) ∪ (a^⊥ ∩ c)) = (a ∪ (a^⊥ ∩ c))
11	6, 8, 10	3tr 65	. . . . . . 7 ((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) = (a ∪ (a^⊥ ∩ c))
12		an1 106	. . . . . . . . 9 (b ∩ 1) = b
13	2	lan 77	. . . . . . . . . 10 ((b →₁c) ∩ (1 →₁c)) = ((b →₁c) ∩ c)
14		u1lemab 610	. . . . . . . . . 10 ((b →₁c) ∩ c) = ((b ∩ c) ∪ (b^⊥ ∩ c))
15	13, 14	ax-r2 36	. . . . . . . . 9 ((b →₁c) ∩ (1 →₁c)) = ((b ∩ c) ∪ (b^⊥ ∩ c))
16	12, 15	2or 72	. . . . . . . 8 ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c))) = (b ∪ ((b ∩ c) ∪ (b^⊥ ∩ c)))
17		ax-a3 32	. . . . . . . . 9 ((b ∪ (b ∩ c)) ∪ (b^⊥ ∩ c)) = (b ∪ ((b ∩ c) ∪ (b^⊥ ∩ c)))
18	17	ax-r1 35	. . . . . . . 8 (b ∪ ((b ∩ c) ∪ (b^⊥ ∩ c))) = ((b ∪ (b ∩ c)) ∪ (b^⊥ ∩ c))
19		orabs 120	. . . . . . . . 9 (b ∪ (b ∩ c)) = b
20	19	ax-r5 38	. . . . . . . 8 ((b ∪ (b ∩ c)) ∪ (b^⊥ ∩ c)) = (b ∪ (b^⊥ ∩ c))
21	16, 18, 20	3tr 65	. . . . . . 7 ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c))) = (b ∪ (b^⊥ ∩ c))
22	11, 21	2an 79	. . . . . 6 (((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) ∩ ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c)))) = ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))
23	22	lor 70	. . . . 5 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) ∩ ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c))))) = (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c))))
24		or32 82	. . . . 5 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))) = (((a ∩ b) ∪ ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))) ∪ ((a →₁c) ∩ (b →₁c)))
25		leo 158	. . . . . . . . 9 a ≤ (a ∪ (a^⊥ ∩ c))
26		leo 158	. . . . . . . . 9 b ≤ (b ∪ (b^⊥ ∩ c))
27	25, 26	le2an 169	. . . . . . . 8 (a ∩ b) ≤ ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))
28	27	df-le2 131	. . . . . . 7 ((a ∩ b) ∪ ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))) = ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))
29		ax-a1 30	. . . . . . . . . 10 a = a^⊥ ^⊥
30	29	ax-r5 38	. . . . . . . . 9 (a ∪ (a^⊥ ∩ c)) = (a^⊥ ^⊥ ∪ (a^⊥ ∩ c))
31		df-i1 44	. . . . . . . . . 10 (a^⊥ →₁c) = (a^⊥ ^⊥ ∪ (a^⊥ ∩ c))
32	31	ax-r1 35	. . . . . . . . 9 (a^⊥ ^⊥ ∪ (a^⊥ ∩ c)) = (a^⊥ →₁c)
33	30, 32	ax-r2 36	. . . . . . . 8 (a ∪ (a^⊥ ∩ c)) = (a^⊥ →₁c)
34		ax-a1 30	. . . . . . . . . 10 b = b^⊥ ^⊥
35	34	ax-r5 38	. . . . . . . . 9 (b ∪ (b^⊥ ∩ c)) = (b^⊥ ^⊥ ∪ (b^⊥ ∩ c))
36		df-i1 44	. . . . . . . . . 10 (b^⊥ →₁c) = (b^⊥ ^⊥ ∪ (b^⊥ ∩ c))
37	36	ax-r1 35	. . . . . . . . 9 (b^⊥ ^⊥ ∪ (b^⊥ ∩ c)) = (b^⊥ →₁c)
38	35, 37	ax-r2 36	. . . . . . . 8 (b ∪ (b^⊥ ∩ c)) = (b^⊥ →₁c)
39	33, 38	2an 79	. . . . . . 7 ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c))) = ((a^⊥ →₁c) ∩ (b^⊥ →₁c))
40	28, 39	ax-r2 36	. . . . . 6 ((a ∩ b) ∪ ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))) = ((a^⊥ →₁c) ∩ (b^⊥ →₁c))
41	40	ax-r5 38	. . . . 5 (((a ∩ b) ∪ ((a ∪ (a^⊥ ∩ c)) ∩ (b ∪ (b^⊥ ∩ c)))) ∪ ((a →₁c) ∩ (b →₁c))) = (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))
42	23, 24, 41	3tr 65	. . . 4 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) ∩ ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c))))) = (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))
43	42	lan 77	. . 3 (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) ∩ ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c)))))) = (b ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))))
44	43	lor 70	. 2 (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) ∩ ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c))))))) = (a ∪ (b ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))))
45	44	lan 77	1 ((a →₁c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ 1) ∪ ((a →₁c) ∩ (1 →₁c))) ∩ ((b ∩ 1) ∪ ((b →₁c) ∩ (1 →₁c)))))))) = ((a →₁c) ∩ (a ∪ (b ∩ (((a^⊥ →₁c) ∩ (b^⊥ →₁c)) ∪ ((a →₁c) ∩ (b →₁c))))))

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8 →₁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 ax-r3 439

This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i1 44 df-le1 130 df-le2 131 df-c1 132 df-c2 133

This theorem is referenced by: oa3-6to3 987

W3C validator