Theorem grpvrinv

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

	Ref	Expression
Hypotheses	grpvlinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpvlinv.p	⊢ + = ( +g ‘ 𝐺 )
	grpvlinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	grpvlinv.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	grpvrinv	⊢ ( ( 𝐺 ∈ 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		simpll	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ Grp )
6		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 : 𝐼 ⟶ 𝐵 )
7	6	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑋 : 𝐼 ⟶ 𝐵 )
8	7	ffvelrnda	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑥 ) ∈ 𝐵 )
9	1 2 4 3	grprinv	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑥 ) + ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) = 0 )
10	5 8 9	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑥 ) + ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) = 0 )
11	10	mpteq2dva	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑥 ) + ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) )
12		elmapex	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → ( 𝐵 ∈ V ∧ 𝐼 ∈ V ) )
13	12	simprd	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝐼 ∈ V )
14	13	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝐼 ∈ V )
15		fvexd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ∈ V )
16	7	feqmptd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑋 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑥 ) ) )
17	1 3	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝑁 : 𝐵 ⟶ 𝐵 )
18		fcompt	⊢ ( ( 𝑁 : 𝐵 ⟶ 𝐵 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) → ( 𝑁 ∘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
19	17 6 18	syl2an	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑁 ∘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
20	14 8 15 16 19	offval2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f + ( 𝑁 ∘ 𝑋 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑥 ) + ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) ) )
21		fconstmpt	⊢ ( 𝐼 × { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ 0 )
22	21	a1i	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝐼 × { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) )
23	11 20 22	3eqtr4d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f + ( 𝑁 ∘ 𝑋 ) ) = ( 𝐼 × { 0 } ) )