2vwomr2 - Quantum Logic Explorer

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

Theorem 2vwomr2 362

Description: 2-variable WOML rule.

**Hypothesis**
Ref	Expression
2vwomr2.1	(b ∪ (a^⊥ ∩ b^⊥ )) = 1

**Assertion**
Ref	Expression
2vwomr2	(a^⊥ ∪ (a ∩ b)) = 1

**Proof of Theorem 2vwomr2**
Step	Hyp	Ref	Expression
1		ancom 74	. . . 4 (a ∩ b) = (b ∩ a)
2		ax-a1 30	. . . . 5 b = b^⊥ ^⊥
3		ax-a1 30	. . . . 5 a = a^⊥ ^⊥
4	2, 3	2an 79	. . . 4 (b ∩ a) = (b^⊥ ^⊥ ∩ a^⊥ ^⊥ )
5	1, 4	ax-r2 36	. . 3 (a ∩ b) = (b^⊥ ^⊥ ∩ a^⊥ ^⊥ )
6	5	lor 70	. 2 (a^⊥ ∪ (a ∩ b)) = (a^⊥ ∪ (b^⊥ ^⊥ ∩ a^⊥ ^⊥ ))
7		ancom 74	. . . . . 6 (a^⊥ ∩ b^⊥ ) = (b^⊥ ∩ a^⊥ )
8	2, 7	2or 72	. . . . 5 (b ∪ (a^⊥ ∩ b^⊥ )) = (b^⊥ ^⊥ ∪ (b^⊥ ∩ a^⊥ ))
9	8	ax-r1 35	. . . 4 (b^⊥ ^⊥ ∪ (b^⊥ ∩ a^⊥ )) = (b ∪ (a^⊥ ∩ b^⊥ ))
10		2vwomr2.1	. . . 4 (b ∪ (a^⊥ ∩ b^⊥ )) = 1
11	9, 10	ax-r2 36	. . 3 (b^⊥ ^⊥ ∪ (b^⊥ ∩ a^⊥ )) = 1
12	11	ax-wom 361	. 2 (a^⊥ ∪ (b^⊥ ^⊥ ∩ a^⊥ ^⊥ )) = 1
13	6, 12	ax-r2 36	1 (a^⊥ ∪ (a ∩ b)) = 1

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8

This theorem was proved from axioms: ax-a1 30 ax-a2 31 ax-r1 35 ax-r2 36 ax-r4 37 ax-r5 38 ax-wom 361

This theorem depends on definitions: df-a 40

This theorem is referenced by: 2vwomr2a 364 2vwomlem 365