Metamath Proof Explorer

Theorem pwsmgp

Description: The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Hypotheses pwsmgp.y 
|- Y = ( R ^s I )
pwsmgp.m 
|- M = ( mulGrp ` R )
pwsmgp.z 
|- Z = ( M ^s I )
pwsmgp.n 
|- N = ( mulGrp ` Y )
pwsmgp.b 
|- B = ( Base ` N )
pwsmgp.c 
|- C = ( Base ` Z )
pwsmgp.p 
|- .+ = ( +g ` N )
pwsmgp.q 
|- .+b = ( +g ` Z )
Assertion pwsmgp 
|- ( ( R e. V /\ I e. W ) -> ( B = C /\ .+ = .+b ) )

Proof

Step Hyp Ref Expression
1 pwsmgp.y 
 |-  Y = ( R ^s I )
2 pwsmgp.m 
 |-  M = ( mulGrp ` R )
3 pwsmgp.z 
 |-  Z = ( M ^s I )
4 pwsmgp.n 
 |-  N = ( mulGrp ` Y )
5 pwsmgp.b 
 |-  B = ( Base ` N )
6 pwsmgp.c 
 |-  C = ( Base ` Z )
7 pwsmgp.p 
 |-  .+ = ( +g ` N )
8 pwsmgp.q 
 |-  .+b = ( +g ` Z )
9 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
10 eqid 
 |-  ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
11 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) = ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) )
12 simpr 
 |-  ( ( R e. V /\ I e. W ) -> I e. W )
13 fvexd 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` R ) e. _V )
14 fnconstg 
 |-  ( R e. V -> ( I X. { R } ) Fn I )
15 14 adantr 
 |-  ( ( R e. V /\ I e. W ) -> ( I X. { R } ) Fn I )
16 9 10 11 12 13 15 prdsmgp 
 |-  ( ( R e. V /\ I e. W ) -> ( ( Base ` ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) ) /\ ( +g ` ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) = ( +g ` ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) ) ) )
17 16 simpld 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) ) )
18 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
19 1 18 pwsval 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
20 19 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( mulGrp ` Y ) = ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
21 4 20 eqtrid 
 |-  ( ( R e. V /\ I e. W ) -> N = ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
22 21 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` N ) = ( Base ` ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) )
23 2 fvexi 
 |-  M e. _V
24 eqid 
 |-  ( M ^s I ) = ( M ^s I )
25 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
26 24 25 pwsval 
 |-  ( ( M e. _V /\ I e. W ) -> ( M ^s I ) = ( ( Scalar ` M ) Xs_ ( I X. { M } ) ) )
27 23 12 26 sylancr 
 |-  ( ( R e. V /\ I e. W ) -> ( M ^s I ) = ( ( Scalar ` M ) Xs_ ( I X. { M } ) ) )
28 2 18 mgpsca 
 |-  ( Scalar ` R ) = ( Scalar ` M )
29 28 eqcomi 
 |-  ( Scalar ` M ) = ( Scalar ` R )
30 29 a1i 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` M ) = ( Scalar ` R ) )
31 2 sneqi 
 |-  { M } = { ( mulGrp ` R ) }
32 31 xpeq2i 
 |-  ( I X. { M } ) = ( I X. { ( mulGrp ` R ) } )
33 fnmgp 
 |-  mulGrp Fn _V
34 elex 
 |-  ( R e. V -> R e. _V )
35 34 adantr 
 |-  ( ( R e. V /\ I e. W ) -> R e. _V )
36 fcoconst 
 |-  ( ( mulGrp Fn _V /\ R e. _V ) -> ( mulGrp o. ( I X. { R } ) ) = ( I X. { ( mulGrp ` R ) } ) )
37 33 35 36 sylancr 
 |-  ( ( R e. V /\ I e. W ) -> ( mulGrp o. ( I X. { R } ) ) = ( I X. { ( mulGrp ` R ) } ) )
38 32 37 eqtr4id 
 |-  ( ( R e. V /\ I e. W ) -> ( I X. { M } ) = ( mulGrp o. ( I X. { R } ) ) )
39 30 38 oveq12d 
 |-  ( ( R e. V /\ I e. W ) -> ( ( Scalar ` M ) Xs_ ( I X. { M } ) ) = ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) )
40 27 39 eqtrd 
 |-  ( ( R e. V /\ I e. W ) -> ( M ^s I ) = ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) )
41 3 40 eqtrid 
 |-  ( ( R e. V /\ I e. W ) -> Z = ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) )
42 41 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` Z ) = ( Base ` ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) ) )
43 17 22 42 3eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` N ) = ( Base ` Z ) )
44 43 5 6 3eqtr4g 
 |-  ( ( R e. V /\ I e. W ) -> B = C )
45 16 simprd 
 |-  ( ( R e. V /\ I e. W ) -> ( +g ` ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) = ( +g ` ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) ) )
46 21 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( +g ` N ) = ( +g ` ( mulGrp ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) )
47 41 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( +g ` Z ) = ( +g ` ( ( Scalar ` R ) Xs_ ( mulGrp o. ( I X. { R } ) ) ) ) )
48 45 46 47 3eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> ( +g ` N ) = ( +g ` Z ) )
49 48 7 8 3eqtr4g 
 |-  ( ( R e. V /\ I e. W ) -> .+ = .+b )
50 44 49 jca 
 |-  ( ( R e. V /\ I e. W ) -> ( B = C /\ .+ = .+b ) )