Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem axoa4a 1016

Description: Proper 4-variable OA law variant.

**Assertion**
Ref	Expression
axoa4a	((a →₁d) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))))))) ≤ (((a ∩ d) ∪ (b ∩ d)) ∪ (c ∩ d))

**Proof of Theorem axoa4a**
Step	Hyp	Ref	Expression
1		id 58	. 2 (a →₁d)^⊥ = (a →₁d)^⊥
2		id 58	. 2 (b →₁d)^⊥ = (b →₁d)^⊥
3		id 58	. 2 (c →₁d)^⊥ = (c →₁d)^⊥
4		leo 150	. . . 4 a^⊥ ≤ (a^⊥ ∪ (a ∩ d))
5		df-i1 43	. . . . . 6 (a →₁d) = (a^⊥ ∪ (a ∩ d))
6	5	ax-r1 34	. . . . 5 (a^⊥ ∪ (a ∩ d)) = (a →₁d)
7		ax-a1 29	. . . . 5 (a →₁d) = (a →₁d)^⊥ ^⊥
8	6, 7	ax-r2 35	. . . 4 (a^⊥ ∪ (a ∩ d)) = (a →₁d)^⊥ ^⊥
9	4, 8	lbtr 131	. . 3 a^⊥ ≤ (a →₁d)^⊥ ^⊥
10		leo 150	. . . 4 b^⊥ ≤ (b^⊥ ∪ (b ∩ d))
11		df-i1 43	. . . . . 6 (b →₁d) = (b^⊥ ∪ (b ∩ d))
12	11	ax-r1 34	. . . . 5 (b^⊥ ∪ (b ∩ d)) = (b →₁d)
13		ax-a1 29	. . . . 5 (b →₁d) = (b →₁d)^⊥ ^⊥
14	12, 13	ax-r2 35	. . . 4 (b^⊥ ∪ (b ∩ d)) = (b →₁d)^⊥ ^⊥
15	10, 14	lbtr 131	. . 3 b^⊥ ≤ (b →₁d)^⊥ ^⊥
16		leo 150	. . . 4 c^⊥ ≤ (c^⊥ ∪ (c ∩ d))
17		df-i1 43	. . . . . 6 (c →₁d) = (c^⊥ ∪ (c ∩ d))
18	17	ax-r1 34	. . . . 5 (c^⊥ ∪ (c ∩ d)) = (c →₁d)
19		ax-a1 29	. . . . 5 (c →₁d) = (c →₁d)^⊥ ^⊥
20	18, 19	ax-r2 35	. . . 4 (c^⊥ ∪ (c ∩ d)) = (c →₁d)^⊥ ^⊥
21	16, 20	lbtr 131	. . 3 c^⊥ ≤ (c →₁d)^⊥ ^⊥
22	9, 15, 21	oa6 1015	. 2 (((a^⊥ ∪ (a →₁d)^⊥ ) ∩ (b^⊥ ∪ (b →₁d)^⊥ )) ∩ (c^⊥ ∪ (c →₁d)^⊥ )) ≤ ((a →₁d)^⊥ ∪ (a^⊥ ∩ (b^⊥ ∪ (((a^⊥ ∪ b^⊥ ) ∩ ((a →₁d)^⊥ ∪ (b →₁d)^⊥ )) ∩ (((a^⊥ ∪ c^⊥ ) ∩ ((a →₁d)^⊥ ∪ (c →₁d)^⊥ )) ∪ ((b^⊥ ∪ c^⊥ ) ∩ ((b →₁d)^⊥ ∪ (c →₁d)^⊥ )))))))
23	1, 2, 3, 22	oa6to4 938	1 ((a →₁d) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))))))) ≤ (((a ∩ d) ∪ (b ∩ d)) ∪ (c ∩ d))

Colors of variables: term

Syntax hints: ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₁wi1 13

This theorem is referenced by: 4oa 1018

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 ax-4oa 1012

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i1 43 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org