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 ) )