Metamath Proof Explorer

Theorem chjassi

Description: Associative law for Hilbert lattice join. From definition of lattice in Kalmbach p. 14. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	ch0le.1	$⊢ A \in C_{ℋ}$
		chjcl.2	$⊢ B \in C_{ℋ}$
		chjass.3	$⊢ C \in C_{ℋ}$
	Assertion	chjassi	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} C = A \lor_{ℋ} (B \lor_{ℋ} C)$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		chjcl.2	$⊢ B \in C_{ℋ}$
3		chjass.3	$⊢ C \in C_{ℋ}$
4		inass	$⊢ (⊥ (A) \cap ⊥ (B)) \cap ⊥ (C) = ⊥ (A) \cap (⊥ (B) \cap ⊥ (C))$
5	1 2	chdmj1i	$⊢ ⊥ (A \lor_{ℋ} B) = ⊥ (A) \cap ⊥ (B)$
6	5	ineq1i	$⊢ ⊥ (A \lor_{ℋ} B) \cap ⊥ (C) = (⊥ (A) \cap ⊥ (B)) \cap ⊥ (C)$
7	2 3	chdmj1i	$⊢ ⊥ (B \lor_{ℋ} C) = ⊥ (B) \cap ⊥ (C)$
8	7	ineq2i	$⊢ ⊥ (A) \cap ⊥ (B \lor_{ℋ} C) = ⊥ (A) \cap (⊥ (B) \cap ⊥ (C))$
9	4 6 8	3eqtr4i	$⊢ ⊥ (A \lor_{ℋ} B) \cap ⊥ (C) = ⊥ (A) \cap ⊥ (B \lor_{ℋ} C)$
10	9	fveq2i	$⊢ ⊥ (⊥ (A \lor_{ℋ} B) \cap ⊥ (C)) = ⊥ (⊥ (A) \cap ⊥ (B \lor_{ℋ} C))$
11	1 2	chjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
12	11 3	chdmm4i	$⊢ ⊥ (⊥ (A \lor_{ℋ} B) \cap ⊥ (C)) = (A \lor_{ℋ} B) \lor_{ℋ} C$
13	2 3	chjcli	$⊢ B \lor_{ℋ} C \in C_{ℋ}$
14	1 13	chdmm4i	$⊢ ⊥ (⊥ (A) \cap ⊥ (B \lor_{ℋ} C)) = A \lor_{ℋ} (B \lor_{ℋ} C)$
15	10 12 14	3eqtr3i	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} C = A \lor_{ℋ} (B \lor_{ℋ} C)$