Metamath Proof Explorer

Theorem mulgfvi

Description: The group multiple operation is compatible with identity-function protection. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis mulgfvi.t 
|- .x. = ( .g ` G )
Assertion mulgfvi 
|- .x. = ( .g ` ( _I ` G ) )

Proof

Step Hyp Ref Expression
1 mulgfvi.t 
 |-  .x. = ( .g ` G )
2 fvi 
 |-  ( G e. _V -> ( _I ` G ) = G )
3 2 eqcomd 
 |-  ( G e. _V -> G = ( _I ` G ) )
4 3 fveq2d 
 |-  ( G e. _V -> ( .g ` G ) = ( .g ` ( _I ` G ) ) )
5 fvprc 
 |-  ( -. G e. _V -> ( .g ` G ) = (/) )
6 fvprc 
 |-  ( -. G e. _V -> ( _I ` G ) = (/) )
7 6 fveq2d 
 |-  ( -. G e. _V -> ( .g ` ( _I ` G ) ) = ( .g ` (/) ) )
8 base0 
 |-  (/) = ( Base ` (/) )
9 eqid 
 |-  ( .g ` (/) ) = ( .g ` (/) )
10 8 9 mulgfn 
 |-  ( .g ` (/) ) Fn ( ZZ X. (/) )
11 xp0 
 |-  ( ZZ X. (/) ) = (/)
12 11 fneq2i 
 |-  ( ( .g ` (/) ) Fn ( ZZ X. (/) ) <-> ( .g ` (/) ) Fn (/) )
13 10 12 mpbi 
 |-  ( .g ` (/) ) Fn (/)
14 fn0 
 |-  ( ( .g ` (/) ) Fn (/) <-> ( .g ` (/) ) = (/) )
15 13 14 mpbi 
 |-  ( .g ` (/) ) = (/)
16 7 15 eqtrdi 
 |-  ( -. G e. _V -> ( .g ` ( _I ` G ) ) = (/) )
17 5 16 eqtr4d 
 |-  ( -. G e. _V -> ( .g ` G ) = ( .g ` ( _I ` G ) ) )
18 4 17 pm2.61i 
 |-  ( .g ` G ) = ( .g ` ( _I ` G ) )
19 1 18 eqtri 
 |-  .x. = ( .g ` ( _I ` G ) )