This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmbr

Description: Binary relation expressing A commutes with B . Definition of commutes in Kalmbach p. 20. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	cmbr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} B \leftrightarrow A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)))$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ x = A \to (x \in C_{ℋ} \leftrightarrow A \in C_{ℋ})$
2	1	anbi1d	$⊢ x = A \to ((x \in C_{ℋ} \land y \in C_{ℋ}) \leftrightarrow (A \in C_{ℋ} \land y \in C_{ℋ}))$
3		id	$⊢ x = A \to x = A$
4		ineq1	$⊢ x = A \to x \cap y = A \cap y$
5		ineq1	$⊢ x = A \to x \cap ⊥ (y) = A \cap ⊥ (y)$
6	4 5	oveq12d	$⊢ x = A \to (x \cap y) \lor_{ℋ} (x \cap ⊥ (y)) = (A \cap y) \lor_{ℋ} (A \cap ⊥ (y))$
7	3 6	eqeq12d	$⊢ x = A \to (x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y)) \leftrightarrow A = (A \cap y) \lor_{ℋ} (A \cap ⊥ (y)))$
8	2 7	anbi12d	$⊢ x = A \to (((x \in C_{ℋ} \land y \in C_{ℋ}) \land x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y))) \leftrightarrow ((A \in C_{ℋ} \land y \in C_{ℋ}) \land A = (A \cap y) \lor_{ℋ} (A \cap ⊥ (y))))$
9		eleq1	$⊢ y = B \to (y \in C_{ℋ} \leftrightarrow B \in C_{ℋ})$
10	9	anbi2d	$⊢ y = B \to ((A \in C_{ℋ} \land y \in C_{ℋ}) \leftrightarrow (A \in C_{ℋ} \land B \in C_{ℋ}))$
11		ineq2	$⊢ y = B \to A \cap y = A \cap B$
12		fveq2	$⊢ y = B \to ⊥ (y) = ⊥ (B)$
13	12	ineq2d	$⊢ y = B \to A \cap ⊥ (y) = A \cap ⊥ (B)$
14	11 13	oveq12d	$⊢ y = B \to (A \cap y) \lor_{ℋ} (A \cap ⊥ (y)) = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
15	14	eqeq2d	$⊢ y = B \to (A = (A \cap y) \lor_{ℋ} (A \cap ⊥ (y)) \leftrightarrow A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)))$
16	10 15	anbi12d	$⊢ y = B \to (((A \in C_{ℋ} \land y \in C_{ℋ}) \land A = (A \cap y) \lor_{ℋ} (A \cap ⊥ (y))) \leftrightarrow ((A \in C_{ℋ} \land B \in C_{ℋ}) \land A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))))$
17		df-cm	$⊢ 𝐶_{ℋ} = \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y)))\}$
18	8 16 17	brabg	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} B \leftrightarrow ((A \in C_{ℋ} \land B \in C_{ℋ}) \land A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))))$
19	18	bianabs	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} B \leftrightarrow A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)))$