Theorem grpvlinv

Description: Tuple-wise left inverse in groups. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	grpvlinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpvlinv.p	⊢ + = ( +g ‘ 𝐺 )
	grpvlinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	grpvlinv.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	grpvlinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ( 𝑁 ∘ 𝑋 ) ∘f + 𝑋 ) = ( 𝐼 × { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		grpvlinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpvlinv.p	⊢ + = ( +g ‘ 𝐺 )
3		grpvlinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
4		grpvlinv.z	⊢ 0 = ( 0g ‘ 𝐺 )
5		elmapex	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → ( 𝐵 ∈ V ∧ 𝐼 ∈ V ) )
6	5	simprd	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝐼 ∈ V )
7	6	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝐼 ∈ V )
8		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 : 𝐼 ⟶ 𝐵 )
9	8	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑋 : 𝐼 ⟶ 𝐵 )
10	1 4	grpidcl	⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
11	10	adantr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → 0 ∈ 𝐵 )
12	1 3	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝑁 : 𝐵 ⟶ 𝐵 )
13	12	adantr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑁 : 𝐵 ⟶ 𝐵 )
14		fcompt	⊢ ( ( 𝑁 : 𝐵 ⟶ 𝐵 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) → ( 𝑁 ∘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
15	12 8 14	syl2an	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑁 ∘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
16	1 2 4 3	grplinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑦 ) + 𝑦 ) = 0 )
17	16	adantlr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑦 ) + 𝑦 ) = 0 )
18	7 9 11 13 15 17	caofinvl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ( 𝑁 ∘ 𝑋 ) ∘f + 𝑋 ) = ( 𝐼 × { 0 } ) )