| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iftrue 4530 | . . . . 5
⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) = 𝑋) | 
| 2 | 1 | eleq1d 2825 | . . . 4
⊢ (𝑥 = (𝐼 × {0}) → (if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) ∈ (Base‘𝐻) ↔ 𝑋 ∈ (Base‘𝐻))) | 
| 3 |  | eqid 2736 | . . . . . 6
⊢ (𝐼 mPwSer 𝐻) = (𝐼 mPwSer 𝐻) | 
| 4 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 5 |  | eqid 2736 | . . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} | 
| 6 |  | eqid 2736 | . . . . . 6
⊢
(Base‘(𝐼
mPwSer 𝐻)) =
(Base‘(𝐼 mPwSer 𝐻)) | 
| 7 |  | subrgascl.p | . . . . . . . . 9
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 8 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 9 |  | subrgasclcl.k | . . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) | 
| 10 |  | subrgascl.a | . . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) | 
| 11 |  | subrgascl.i | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 12 |  | subrgascl.r | . . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) | 
| 13 |  | subrgrcl 20577 | . . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | 
| 14 | 12, 13 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 15 |  | subrgasclcl.x | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐾) | 
| 16 | 7, 5, 8, 9, 10, 11, 14, 15 | mplascl 22089 | . . . . . . . 8
⊢ (𝜑 → (𝐴‘𝑋) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)))) | 
| 17 | 16 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝐴‘𝑋) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)))) | 
| 18 |  | subrgascl.u | . . . . . . . . . 10
⊢ 𝑈 = (𝐼 mPoly 𝐻) | 
| 19 |  | subrgasclcl.b | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑈) | 
| 20 |  | subrgascl.h | . . . . . . . . . . . 12
⊢ 𝐻 = (𝑅 ↾s 𝑇) | 
| 21 | 20 | subrgring 20575 | . . . . . . . . . . 11
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝐻 ∈ Ring) | 
| 22 | 12, 21 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ Ring) | 
| 23 | 3, 18, 19, 11, 22 | mplsubrg 22026 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝐻))) | 
| 24 | 6 | subrgss 20573 | . . . . . . . . 9
⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝐻)) → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝐻))) | 
| 25 | 23, 24 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝐻))) | 
| 26 | 25 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝐴‘𝑋) ∈ (Base‘(𝐼 mPwSer 𝐻))) | 
| 27 | 17, 26 | eqeltrrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))) ∈ (Base‘(𝐼 mPwSer 𝐻))) | 
| 28 | 3, 4, 5, 6, 27 | psrelbas 21955 | . . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) | 
| 29 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))) | 
| 30 | 29 | fmpt 7129 | . . . . 5
⊢
(∀𝑥 ∈
{𝑓 ∈
(ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) ∈ (Base‘𝐻) ↔ (𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) | 
| 31 | 28, 30 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → ∀𝑥 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) ∈ (Base‘𝐻)) | 
| 32 | 11 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝐼 ∈ 𝑊) | 
| 33 | 5 | psrbag0 22087 | . . . . 5
⊢ (𝐼 ∈ 𝑊 → (𝐼 × {0}) ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) | 
| 34 | 32, 33 | syl 17 | . . . 4
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝐼 × {0}) ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) | 
| 35 | 2, 31, 34 | rspcdva 3622 | . . 3
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝑋 ∈ (Base‘𝐻)) | 
| 36 | 20 | subrgbas 20582 | . . . . 5
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 = (Base‘𝐻)) | 
| 37 | 12, 36 | syl 17 | . . . 4
⊢ (𝜑 → 𝑇 = (Base‘𝐻)) | 
| 38 | 37 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝑇 = (Base‘𝐻)) | 
| 39 | 35, 38 | eleqtrrd 2843 | . 2
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝑋 ∈ 𝑇) | 
| 40 |  | eqid 2736 | . . . . . 6
⊢
(algSc‘𝑈) =
(algSc‘𝑈) | 
| 41 | 7, 10, 20, 18, 11, 12, 40 | subrgascl 22091 | . . . . 5
⊢ (𝜑 → (algSc‘𝑈) = (𝐴 ↾ 𝑇)) | 
| 42 | 41 | fveq1d 6907 | . . . 4
⊢ (𝜑 → ((algSc‘𝑈)‘𝑋) = ((𝐴 ↾ 𝑇)‘𝑋)) | 
| 43 |  | fvres 6924 | . . . 4
⊢ (𝑋 ∈ 𝑇 → ((𝐴 ↾ 𝑇)‘𝑋) = (𝐴‘𝑋)) | 
| 44 | 42, 43 | sylan9eq 2796 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → ((algSc‘𝑈)‘𝑋) = (𝐴‘𝑋)) | 
| 45 |  | eqid 2736 | . . . . . . 7
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) | 
| 46 | 18 | mplring 22040 | . . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝐻 ∈ Ring) → 𝑈 ∈ Ring) | 
| 47 | 18 | mpllmod 22039 | . . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝐻 ∈ Ring) → 𝑈 ∈ LMod) | 
| 48 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) | 
| 49 | 40, 45, 46, 47, 48, 19 | asclf 21903 | . . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ 𝐻 ∈ Ring) → (algSc‘𝑈):(Base‘(Scalar‘𝑈))⟶𝐵) | 
| 50 | 11, 22, 49 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (algSc‘𝑈):(Base‘(Scalar‘𝑈))⟶𝐵) | 
| 51 | 50 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → (algSc‘𝑈):(Base‘(Scalar‘𝑈))⟶𝐵) | 
| 52 | 18, 11, 22 | mplsca 22034 | . . . . . . . 8
⊢ (𝜑 → 𝐻 = (Scalar‘𝑈)) | 
| 53 | 52 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 → (Base‘𝐻) =
(Base‘(Scalar‘𝑈))) | 
| 54 | 37, 53 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → 𝑇 = (Base‘(Scalar‘𝑈))) | 
| 55 | 54 | eleq2d 2826 | . . . . 5
⊢ (𝜑 → (𝑋 ∈ 𝑇 ↔ 𝑋 ∈ (Base‘(Scalar‘𝑈)))) | 
| 56 | 55 | biimpa 476 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → 𝑋 ∈ (Base‘(Scalar‘𝑈))) | 
| 57 | 51, 56 | ffvelcdmd 7104 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → ((algSc‘𝑈)‘𝑋) ∈ 𝐵) | 
| 58 | 44, 57 | eqeltrrd 2841 | . 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → (𝐴‘𝑋) ∈ 𝐵) | 
| 59 | 39, 58 | impbida 800 | 1
⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇)) |