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

Metamath Proof Explorer

Theorem symgov

Description: The value of the group operation of the symmetric group on A . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015) (Revised by AV, 30-Mar-2024)

		Ref	Expression
	Hypotheses	symgov.1	$⊢ G = SymGrp (A)$
		symgov.2	$⊢ B = {Base}_{G}$
		symgov.3	$⊢ \underset{˙}{+} = +_{G}$
	Assertion	symgov	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X \circ Y$

Proof

Step	Hyp	Ref	Expression
1		symgov.1	$⊢ G = SymGrp (A)$
2		symgov.2	$⊢ B = {Base}_{G}$
3		symgov.3	$⊢ \underset{˙}{+} = +_{G}$
4		eqid	$⊢ A^{A} = A^{A}$
5	1 4 3	symgplusg	$⊢ \underset{˙}{+} = (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)$
6	5	a1i	$⊢ (X \in B \land Y \in B) \to \underset{˙}{+} = (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)$
7		simpl	$⊢ (f = X \land g = Y) \to f = X$
8		simpr	$⊢ (f = X \land g = Y) \to g = Y$
9	7 8	coeq12d	$⊢ (f = X \land g = Y) \to f \circ g = X \circ Y$
10	9	adantl	$⊢ ((X \in B \land Y \in B) \land (f = X \land g = Y)) \to f \circ g = X \circ Y$
11	1 2	symgbasmap	$⊢ X \in B \to X \in (A^{A})$
12	11	adantr	$⊢ (X \in B \land Y \in B) \to X \in (A^{A})$
13	1 2	symgbasmap	$⊢ Y \in B \to Y \in (A^{A})$
14	13	adantl	$⊢ (X \in B \land Y \in B) \to Y \in (A^{A})$
15		coexg	$⊢ (X \in B \land Y \in B) \to X \circ Y \in V$
16	6 10 12 14 15	ovmpod	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X \circ Y$