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

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( ( 𝐺 ∈ 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 } ) )