Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` G )
grpvlinv.n 
|- N = ( invg ` G )
grpvlinv.z 
|- .0. = ( 0g ` G )
Assertion grpvlinv 
|- ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( ( N o. X ) oF .+ 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 elmapex 
 |-  ( X e. ( B ^m I ) -> ( B e. _V /\ I e. _V ) )
6 5 simprd 
 |-  ( X e. ( B ^m I ) -> I e. _V )
7 6 adantl 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> I e. _V )
8 elmapi 
 |-  ( X e. ( B ^m I ) -> X : I --> B )
9 8 adantl 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> X : I --> B )
10 1 4 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
11 10 adantr 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> .0. e. B )
12 1 3 grpinvf 
 |-  ( G e. Grp -> N : B --> B )
13 12 adantr 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> N : B --> B )
14 fcompt 
 |-  ( ( N : B --> B /\ X : I --> B ) -> ( N o. X ) = ( x e. I |-> ( N ` ( X ` x ) ) ) )
15 12 8 14 syl2an 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( N o. X ) = ( x e. I |-> ( N ` ( X ` x ) ) ) )
16 1 2 4 3 grplinv 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( N ` y ) .+ y ) = .0. )
17 16 adantlr 
 |-  ( ( ( G e. Grp /\ X e. ( B ^m I ) ) /\ y e. B ) -> ( ( N ` y ) .+ y ) = .0. )
18 7 9 11 13 15 17 caofinvl 
 |-  ( ( G e. Grp /\ X e. ( B ^m I ) ) -> ( ( N o. X ) oF .+ X ) = ( I X. { .0. } ) )