Metamath Proof Explorer

Theorem mplbaspropd

Description: Property deduction for polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 19-Jul-2019)

Ref Expression
Hypotheses psrplusgpropd.b1 
|- ( ph -> B = ( Base ` R ) )
psrplusgpropd.b2 
|- ( ph -> B = ( Base ` S ) )
psrplusgpropd.p 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
Assertion mplbaspropd 
|- ( ph -> ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly S ) ) )

Proof

Step Hyp Ref Expression
1 psrplusgpropd.b1 
 |-  ( ph -> B = ( Base ` R ) )
2 psrplusgpropd.b2 
 |-  ( ph -> B = ( Base ` S ) )
3 psrplusgpropd.p 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
4 1 2 eqtr3d 
 |-  ( ph -> ( Base ` R ) = ( Base ` S ) )
5 4 psrbaspropd 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
6 5 adantr 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
7 1 2 3 grpidpropd 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` S ) )
8 7 breq2d 
 |-  ( ph -> ( a finSupp ( 0g ` R ) <-> a finSupp ( 0g ` S ) ) )
9 8 adantr 
 |-  ( ( ph /\ I e. _V ) -> ( a finSupp ( 0g ` R ) <-> a finSupp ( 0g ` S ) ) )
10 6 9 rabeqbidv 
 |-  ( ( ph /\ I e. _V ) -> { a e. ( Base ` ( I mPwSer R ) ) | a finSupp ( 0g ` R ) } = { a e. ( Base ` ( I mPwSer S ) ) | a finSupp ( 0g ` S ) } )
11 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
12 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
13 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 eqid 
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
16 11 12 13 14 15 mplbas 
 |-  ( Base ` ( I mPoly R ) ) = { a e. ( Base ` ( I mPwSer R ) ) | a finSupp ( 0g ` R ) }
17 eqid 
 |-  ( I mPoly S ) = ( I mPoly S )
18 eqid 
 |-  ( I mPwSer S ) = ( I mPwSer S )
19 eqid 
 |-  ( Base ` ( I mPwSer S ) ) = ( Base ` ( I mPwSer S ) )
20 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
21 eqid 
 |-  ( Base ` ( I mPoly S ) ) = ( Base ` ( I mPoly S ) )
22 17 18 19 20 21 mplbas 
 |-  ( Base ` ( I mPoly S ) ) = { a e. ( Base ` ( I mPwSer S ) ) | a finSupp ( 0g ` S ) }
23 10 16 22 3eqtr4g 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly S ) ) )
24 reldmmpl 
 |-  Rel dom mPoly
25 24 ovprc1 
 |-  ( -. I e. _V -> ( I mPoly R ) = (/) )
26 24 ovprc1 
 |-  ( -. I e. _V -> ( I mPoly S ) = (/) )
27 25 26 eqtr4d 
 |-  ( -. I e. _V -> ( I mPoly R ) = ( I mPoly S ) )
28 27 fveq2d 
 |-  ( -. I e. _V -> ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly S ) ) )
29 28 adantl 
 |-  ( ( ph /\ -. I e. _V ) -> ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly S ) ) )
30 23 29 pm2.61dan 
 |-  ( ph -> ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly S ) ) )