Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` G )
grpvlinv.n 
|- N = ( invg ` G )
grpvlinv.z 
|- .0. = ( 0g ` G )
Assertion grpvrinv 
|- ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( X oF .+ ( N o. X ) ) = ( I X. { .0. } ) )

Proof

Step Hyp Ref Expression
1 grpvlinv.b 
 |-  B = ( Base ` G )
2 grpvlinv.p 
 |-  .+ = ( +g ` G )
3 grpvlinv.n 
 |-  N = ( invg ` G )
4 grpvlinv.z 
 |-  .0. = ( 0g ` G )
5 simpll 
 |-  ( ( ( G e. Grp /\ X e. ( B ^m I ) ) /\ x e. I ) -> G e. Grp )
6 elmapi 
 |-  ( X e. ( B ^m I ) -> X : I --> B )
7 6 adantl 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> X : I --> B )
8 7 ffvelrnda 
 |-  ( ( ( G e. Grp /\ X e. ( B ^m I ) ) /\ x e. I ) -> ( X ` x ) e. B )
9 1 2 4 3 grprinv 
 |-  ( ( G e. Grp /\ ( X ` x ) e. B ) -> ( ( X ` x ) .+ ( N ` ( X ` x ) ) ) = .0. )
10 5 8 9 syl2anc 
 |-  ( ( ( G e. Grp /\ X e. ( B ^m I ) ) /\ x e. I ) -> ( ( X ` x ) .+ ( N ` ( X ` x ) ) ) = .0. )
11 10 mpteq2dva 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( x e. I |-> ( ( X ` x ) .+ ( N ` ( X ` x ) ) ) ) = ( x e. I |-> .0. ) )
12 elmapex 
 |-  ( X e. ( B ^m I ) -> ( B e. _V /\ I e. _V ) )
13 12 simprd 
 |-  ( X e. ( B ^m I ) -> I e. _V )
14 13 adantl 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> I e. _V )
15 fvexd 
 |-  ( ( ( G e. Grp /\ X e. ( B ^m I ) ) /\ x e. I ) -> ( N ` ( X ` x ) ) e. _V )
16 7 feqmptd 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> X = ( x e. I |-> ( X ` x ) ) )
17 1 3 grpinvf 
 |-  ( G e. Grp -> N : B --> B )
18 fcompt 
 |-  ( ( N : B --> B /\ X : I --> B ) -> ( N o. X ) = ( x e. I |-> ( N ` ( X ` x ) ) ) )
19 17 6 18 syl2an 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( N o. X ) = ( x e. I |-> ( N ` ( X ` x ) ) ) )
20 14 8 15 16 19 offval2 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( X oF .+ ( N o. X ) ) = ( x e. I |-> ( ( X ` x ) .+ ( N ` ( X ` x ) ) ) ) )
21 fconstmpt 
 |-  ( I X. { .0. } ) = ( x e. I |-> .0. )
22 21 a1i 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( I X. { .0. } ) = ( x e. I |-> .0. ) )
23 11 20 22 3eqtr4d 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( X oF .+ ( N o. X ) ) = ( I X. { .0. } ) )