Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oi3oa3 715

Description: An attempt at the OA3 conjecture, which is true if (a ≡ b) = 1. (Contributed by Josiah Burroughs 27-May-04.)

**Hypothesis**
Ref	Expression
oi3oa3.1	1 = (b ≡ a)

**Assertion**
Ref	Expression
oi3oa3	(((a →₁c) ∩ (b →₁c)) ∪ ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c))) = 1

**Proof of Theorem oi3oa3**
Step	Hyp	Ref	Expression
1		oi3oa3.1	. . . . . . . 8 1 = (b ≡ a)
2	1	oi3oa3lem1 714	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b)) = 1
3	2	lan 70	. . . . . 6 ((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = ((a →₁c) ∩ 1)
4		an1 98	. . . . . 6 ((a →₁c) ∩ 1) = (a →₁c)
5	3, 4	ax-r2 35	. . . . 5 ((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = (a →₁c)
6	5	ud1lem0b 248	. . . 4 (((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) = ((a →₁c) →₁c)
7	2	lan 70	. . . . . 6 ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = ((b →₁c) ∩ 1)
8		an1 98	. . . . . 6 ((b →₁c) ∩ 1) = (b →₁c)
9	7, 8	ax-r2 35	. . . . 5 ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = (b →₁c)
10	9	ud1lem0b 248	. . . 4 (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) = ((b →₁c) →₁c)
11	6, 10	2an 72	. . 3 ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c)) = (((a →₁c) →₁c) ∩ ((b →₁c) →₁c))
12	11	lor 66	. 2 (((a →₁c) ∩ (b →₁c)) ∪ ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ (((a →₁c) →₁c) ∩ ((b →₁c) →₁c)))
13		ax-a2 30	. 2 (((a →₁c) ∩ (b →₁c)) ∪ (((a →₁c) →₁c) ∩ ((b →₁c) →₁c))) = ((((a →₁c) →₁c) ∩ ((b →₁c) →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))
14	1	r3a 422	. . . . 5 b = a
15	14	ud1lem0b 248	. . . 4 (b →₁c) = (a →₁c)
16	15	1bi 111	. . 3 1 = ((b →₁c) ≡ (a →₁c))
17	16	oi3oa3lem1 714	. 2 ((((a →₁c) →₁c) ∩ ((b →₁c) →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = 1
18	12, 13, 17	3tr 62	1 (((a →₁c) ∩ (b →₁c)) ∪ ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c))) = 1

Colors of variables: term

Syntax hints: = wb 1 ≡ tb 5 ∪ wo 6 ∩ wa 7 1wt 9 →₁wi1 13

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 ax-r3 421

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

metamath.org