grpvlinv

Description: Tuple-wise left inverse in groups. (Contributed by Stefan O'Rear, 5-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	grpvlinv	$⊢ (G \in Grp \land X \in (B^{I})) \to (N \circ X) {\underset{˙}{+}}_{f} X = I \times \{\underset{˙}{0}\}$

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		elmapex	$⊢ X \in (B^{I}) \to (B \in V \land I \in V)$
6	5	simprd	$⊢ X \in (B^{I}) \to I \in V$
7	6	adantl	$⊢ (G \in Grp \land X \in (B^{I})) \to I \in V$
8		elmapi	$⊢ X \in (B^{I}) \to X : I ⟶ B$
9	8	adantl	$⊢ (G \in Grp \land X \in (B^{I})) \to X : I ⟶ B$
10	1 4	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
11	10	adantr	$⊢ (G \in Grp \land X \in (B^{I})) \to \underset{˙}{0} \in B$
12	1 3	grpinvf	$⊢ G \in Grp \to N : B ⟶ B$
13	12	adantr	$⊢ (G \in Grp \land X \in (B^{I})) \to N : B ⟶ B$
14		fcompt	$⊢ (N : B ⟶ B \land X : I ⟶ B) \to N \circ X = (x \in I ⟼ N (X (x)))$
15	12 8 14	syl2an	$⊢ (G \in Grp \land X \in (B^{I})) \to N \circ X = (x \in I ⟼ N (X (x)))$
16	1 2 4 3	grplinv	$⊢ (G \in Grp \land y \in B) \to N (y) \underset{˙}{+} y = \underset{˙}{0}$
17	16	adantlr	$⊢ ((G \in Grp \land X \in (B^{I})) \land y \in B) \to N (y) \underset{˙}{+} y = \underset{˙}{0}$
18	7 9 11 13 15 17	caofinvl	$⊢ (G \in Grp \land X \in (B^{I})) \to (N \circ X) {\underset{˙}{+}}_{f} X = I \times \{\underset{˙}{0}\}$

Metamath Proof Explorer