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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
psrplusgpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
psrplusgpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
Assertion mplbaspropd ( 𝜑 → ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 psrplusgpropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2 psrplusgpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
3 psrplusgpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
4 1 2 eqtr3d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
5 4 psrbaspropd ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
7 1 2 3 grpidpropd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑆 ) )
8 7 breq2d ⊢ ( 𝜑 → ( 𝑎 finSupp ( 0g ‘ 𝑅 ) ↔ 𝑎 finSupp ( 0g ‘ 𝑆 ) ) )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( 𝑎 finSupp ( 0g ‘ 𝑅 ) ↔ 𝑎 finSupp ( 0g ‘ 𝑆 ) ) )
10 6 9 rabeqbidv ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → { 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } = { 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ∣ 𝑎 finSupp ( 0g ‘ 𝑆 ) } )
11 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
12 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
13 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
14 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
16 11 12 13 14 15 mplbas ⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = { 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) }
17 eqid ⊢ ( 𝐼 mPoly 𝑆 ) = ( 𝐼 mPoly 𝑆 )
18 eqid ⊢ ( 𝐼 mPwSer 𝑆 ) = ( 𝐼 mPwSer 𝑆 )
19 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) )
20 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
21 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) )
22 17 18 19 20 21 mplbas ⊢ ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) = { 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ∣ 𝑎 finSupp ( 0g ‘ 𝑆 ) }
23 10 16 22 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )
24 reldmmpl ⊢ Rel dom mPoly
25 24 ovprc1 ⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 mPoly 𝑅 ) = ∅ )
26 24 ovprc1 ⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 mPoly 𝑆 ) = ∅ )
27 25 26 eqtr4d ⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑆 ) )
28 27 fveq2d ⊢ ( ¬ 𝐼 ∈ V → ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )
29 28 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )
30 23 29 pm2.61dan ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )