qlaxr3i

Description: A variation of the orthomodular law, showing CH is an orthomodular lattice. (This corresponds to axiom "ax-r3" in the Quantum Logic Explorer.) (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	qlaxr3.1	$⊢ A \in C_{ℋ}$
	qlaxr3.2	$⊢ B \in C_{ℋ}$
	qlaxr3.3	$⊢ C \in C_{ℋ}$
	qlaxr3.4	$⊢ C \lor_{ℋ} ⊥ (C) = ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (A \lor_{ℋ} B)$
Assertion	qlaxr3i	$⊢ A = B$

Proof

Step	Hyp	Ref	Expression
1		qlaxr3.1	$⊢ A \in C_{ℋ}$
2		qlaxr3.2	$⊢ B \in C_{ℋ}$
3		qlaxr3.3	$⊢ C \in C_{ℋ}$
4		qlaxr3.4	$⊢ C \lor_{ℋ} ⊥ (C) = ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (A \lor_{ℋ} B)$
5	1 2	chjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
6	5	chshii	$⊢ A \lor_{ℋ} B \in S_{ℋ}$
7	1 2	chub1i	$⊢ A \subseteq A \lor_{ℋ} B$
8		incom	$⊢ (A \lor_{ℋ} B) \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B)$
9	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
10	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
11	1 2	cmj1i	$⊢ A 𝐶_{ℋ} (A \lor_{ℋ} B)$
12	1 5 11	cmcmii	$⊢ (A \lor_{ℋ} B) 𝐶_{ℋ} A$
13	5 1 12	cmcm2ii	$⊢ (A \lor_{ℋ} B) 𝐶_{ℋ} ⊥ (A)$
14	1 2	cmj2i	$⊢ B 𝐶_{ℋ} (A \lor_{ℋ} B)$
15	2 5 14	cmcmii	$⊢ (A \lor_{ℋ} B) 𝐶_{ℋ} B$
16	5 2 15	cmcm2ii	$⊢ (A \lor_{ℋ} B) 𝐶_{ℋ} ⊥ (B)$
17	5 9 10 13 16	fh1i	$⊢ (A \lor_{ℋ} B) \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = ((A \lor_{ℋ} B) \cap ⊥ (A)) \lor_{ℋ} ((A \lor_{ℋ} B) \cap ⊥ (B))$
18	8 17	eqtr3i	$⊢ (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B) = ((A \lor_{ℋ} B) \cap ⊥ (A)) \lor_{ℋ} ((A \lor_{ℋ} B) \cap ⊥ (B))$
19	3	chjoi	$⊢ C \lor_{ℋ} ⊥ (C) = ℋ$
20	19 4	eqtr3i	$⊢ ℋ = ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (A \lor_{ℋ} B)$
21		choc0	$⊢ ⊥ (0_{ℋ}) = ℋ$
22	9 10	chjcli	$⊢ ⊥ (A) \lor_{ℋ} ⊥ (B) \in C_{ℋ}$
23	22 5	chdmm1i	$⊢ ⊥ ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B)) = ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (A \lor_{ℋ} B)$
24	20 21 23	3eqtr4i	$⊢ ⊥ (0_{ℋ}) = ⊥ ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B))$
25	22 5	chincli	$⊢ (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B) \in C_{ℋ}$
26		h0elch	$⊢ 0_{ℋ} \in C_{ℋ}$
27	25 26	chcon3i	$⊢ (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B) = 0_{ℋ} \leftrightarrow ⊥ (0_{ℋ}) = ⊥ ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B))$
28	24 27	mpbir	$⊢ (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (A \lor_{ℋ} B) = 0_{ℋ}$
29	18 28	eqtr3i	$⊢ ((A \lor_{ℋ} B) \cap ⊥ (A)) \lor_{ℋ} ((A \lor_{ℋ} B) \cap ⊥ (B)) = 0_{ℋ}$
30	5 9	chincli	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \in C_{ℋ}$
31	5 10	chincli	$⊢ (A \lor_{ℋ} B) \cap ⊥ (B) \in C_{ℋ}$
32	30 31	chj00i	$⊢ ((A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \land (A \lor_{ℋ} B) \cap ⊥ (B) = 0_{ℋ}) \leftrightarrow ((A \lor_{ℋ} B) \cap ⊥ (A)) \lor_{ℋ} ((A \lor_{ℋ} B) \cap ⊥ (B)) = 0_{ℋ}$
33	29 32	mpbir	$⊢ ((A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \land (A \lor_{ℋ} B) \cap ⊥ (B) = 0_{ℋ})$
34	33	simpli	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ}$
35	1 6 7 34	omlsii	$⊢ A = A \lor_{ℋ} B$
36	2 1	chub2i	$⊢ B \subseteq A \lor_{ℋ} B$
37	33	simpri	$⊢ (A \lor_{ℋ} B) \cap ⊥ (B) = 0_{ℋ}$
38	2 6 36 37	omlsii	$⊢ B = A \lor_{ℋ} B$
39	35 38	eqtr4i	$⊢ A = B$

Metamath Proof Explorer

Theorem qlaxr3i

Proof