grpvrinv

Description: Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	grpvlinv.b	$⊢ B = {Base}_{G}$
	grpvlinv.p	$⊢ \underset{˙}{+} = +_{G}$
	grpvlinv.n	$⊢ N = {inv}_{g} (G)$
	grpvlinv.z	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	grpvrinv	$⊢ (G \in Grp \land X \in (B^{I})) \to X {\underset{˙}{+}}_{f} (N \circ X) = I \times \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		grpvlinv.b	$⊢ B = {Base}_{G}$
2		grpvlinv.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpvlinv.n	$⊢ N = {inv}_{g} (G)$
4		grpvlinv.z	$⊢ \underset{˙}{0} = 0_{G}$
5		simpll	$⊢ ((G \in Grp \land X \in (B^{I})) \land x \in I) \to G \in Grp$
6		elmapi	$⊢ X \in (B^{I}) \to X : I ⟶ B$
7	6	adantl	$⊢ (G \in Grp \land X \in (B^{I})) \to X : I ⟶ B$
8	7	ffvelrnda	$⊢ ((G \in Grp \land X \in (B^{I})) \land x \in I) \to X (x) \in B$
9	1 2 4 3	grprinv	$⊢ (G \in Grp \land X (x) \in B) \to X (x) \underset{˙}{+} N (X (x)) = \underset{˙}{0}$
10	5 8 9	syl2anc	$⊢ ((G \in Grp \land X \in (B^{I})) \land x \in I) \to X (x) \underset{˙}{+} N (X (x)) = \underset{˙}{0}$
11	10	mpteq2dva	$⊢ (G \in Grp \land X \in (B^{I})) \to (x \in I ⟼ X (x) \underset{˙}{+} N (X (x))) = (x \in I ⟼ \underset{˙}{0})$
12		elmapex	$⊢ X \in (B^{I}) \to (B \in V \land I \in V)$
13	12	simprd	$⊢ X \in (B^{I}) \to I \in V$
14	13	adantl	$⊢ (G \in Grp \land X \in (B^{I})) \to I \in V$
15		fvexd	$⊢ ((G \in Grp \land X \in (B^{I})) \land x \in I) \to N (X (x)) \in V$
16	7	feqmptd	$⊢ (G \in Grp \land X \in (B^{I})) \to X = (x \in I ⟼ X (x))$
17	1 3	grpinvf	$⊢ G \in Grp \to N : B ⟶ B$
18		fcompt	$⊢ (N : B ⟶ B \land X : I ⟶ B) \to N \circ X = (x \in I ⟼ N (X (x)))$
19	17 6 18	syl2an	$⊢ (G \in Grp \land X \in (B^{I})) \to N \circ X = (x \in I ⟼ N (X (x)))$
20	14 8 15 16 19	offval2	$⊢ (G \in Grp \land X \in (B^{I})) \to X {\underset{˙}{+}}_{f} (N \circ X) = (x \in I ⟼ X (x) \underset{˙}{+} N (X (x)))$
21		fconstmpt	$⊢ I \times \{\underset{˙}{0}\} = (x \in I ⟼ \underset{˙}{0})$
22	21	a1i	$⊢ (G \in Grp \land X \in (B^{I})) \to I \times \{\underset{˙}{0}\} = (x \in I ⟼ \underset{˙}{0})$
23	11 20 22	3eqtr4d	$⊢ (G \in Grp \land X \in (B^{I})) \to X {\underset{˙}{+}}_{f} (N \circ X) = I \times \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem grpvrinv

Proof