nmzbi

Description: Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

		Ref	Expression
	Hypothesis	elnmz.1	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S)\}$
	Assertion	nmzbi	$⊢ (A \in N \land B \in X) \to (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S)$

Step	Hyp	Ref	Expression
1		elnmz.1	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S)\}$
2	1	elnmz	$⊢ A \in N \leftrightarrow (A \in X \land \forall z \in X (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S))$
3	2	simprbi	$⊢ A \in N \to \forall z \in X (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S)$
4		oveq2	$⊢ z = B \to A \underset{˙}{+} z = A \underset{˙}{+} B$
5	4	eleq1d	$⊢ z = B \to (A \underset{˙}{+} z \in S \leftrightarrow A \underset{˙}{+} B \in S)$
6		oveq1	$⊢ z = B \to z \underset{˙}{+} A = B \underset{˙}{+} A$
7	6	eleq1d	$⊢ z = B \to (z \underset{˙}{+} A \in S \leftrightarrow B \underset{˙}{+} A \in S)$
8	5 7	bibi12d	$⊢ z = B \to ((A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S) \leftrightarrow (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S))$
9	8	rspccva	$⊢ (\forall z \in X (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S) \land B \in X) \to (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S)$
10	3 9	sylan	$⊢ (A \in N \land B \in X) \to (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S)$

Metamath Proof Explorer