Step | Hyp | Ref
| Expression |
1 | | subrgascl.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝐼 ∈ 𝑊) |
3 | | eqid 2610 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
4 | 3 | psrbag0 19315 |
. . . . 5
⊢ (𝐼 ∈ 𝑊 → (𝐼 × {0}) ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
5 | 2, 4 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝐼 × {0}) ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
6 | | eqid 2610 |
. . . . . 6
⊢ (𝐼 mPwSer 𝐻) = (𝐼 mPwSer 𝐻) |
7 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐻) =
(Base‘𝐻) |
8 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(𝐼
mPwSer 𝐻)) =
(Base‘(𝐼 mPwSer 𝐻)) |
9 | | subrgascl.p |
. . . . . . . . 9
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
10 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
11 | | subrgasclcl.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
12 | | subrgascl.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
13 | | subrgascl.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) |
14 | | subrgrcl 18608 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
16 | | subrgasclcl.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐾) |
17 | 9, 3, 10, 11, 12, 1, 15, 16 | mplascl 19317 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝑋) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)))) |
18 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝐴‘𝑋) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)))) |
19 | | subrgascl.u |
. . . . . . . . . 10
⊢ 𝑈 = (𝐼 mPoly 𝐻) |
20 | | subrgasclcl.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑈) |
21 | | subrgascl.h |
. . . . . . . . . . . 12
⊢ 𝐻 = (𝑅 ↾s 𝑇) |
22 | 21 | subrgring 18606 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝐻 ∈ Ring) |
23 | 13, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ Ring) |
24 | 6, 19, 20, 1, 23 | mplsubrg 19261 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝐻))) |
25 | 8 | subrgss 18604 |
. . . . . . . . 9
⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝐻)) → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝐻))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝐻))) |
27 | 26 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝐴‘𝑋) ∈ (Base‘(𝐼 mPwSer 𝐻))) |
28 | 18, 27 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))) ∈ (Base‘(𝐼 mPwSer 𝐻))) |
29 | 6, 7, 3, 8, 28 | psrelbas 19200 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
30 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))) |
31 | 30 | fmpt 6289 |
. . . . 5
⊢
(∀𝑥 ∈
{𝑓 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) ∈ (Base‘𝐻) ↔ (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅))):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
32 | 29, 31 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → ∀𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) ∈ (Base‘𝐻)) |
33 | | iftrue 4042 |
. . . . . 6
⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) = 𝑋) |
34 | 33 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = (𝐼 × {0}) → (if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) ∈ (Base‘𝐻) ↔ 𝑋 ∈ (Base‘𝐻))) |
35 | 34 | rspcv 3278 |
. . . 4
⊢ ((𝐼 × {0}) ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} →
(∀𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}if(𝑥 = (𝐼 × {0}), 𝑋, (0g‘𝑅)) ∈ (Base‘𝐻) → 𝑋 ∈ (Base‘𝐻))) |
36 | 5, 32, 35 | sylc 63 |
. . 3
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝑋 ∈ (Base‘𝐻)) |
37 | 21 | subrgbas 18612 |
. . . . 5
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 = (Base‘𝐻)) |
38 | 13, 37 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇 = (Base‘𝐻)) |
39 | 38 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝑇 = (Base‘𝐻)) |
40 | 36, 39 | eleqtrrd 2691 |
. 2
⊢ ((𝜑 ∧ (𝐴‘𝑋) ∈ 𝐵) → 𝑋 ∈ 𝑇) |
41 | | eqid 2610 |
. . . . . 6
⊢
(algSc‘𝑈) =
(algSc‘𝑈) |
42 | 9, 12, 21, 19, 1, 13, 41 | subrgascl 19319 |
. . . . 5
⊢ (𝜑 → (algSc‘𝑈) = (𝐴 ↾ 𝑇)) |
43 | 42 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → ((algSc‘𝑈)‘𝑋) = ((𝐴 ↾ 𝑇)‘𝑋)) |
44 | | fvres 6117 |
. . . 4
⊢ (𝑋 ∈ 𝑇 → ((𝐴 ↾ 𝑇)‘𝑋) = (𝐴‘𝑋)) |
45 | 43, 44 | sylan9eq 2664 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → ((algSc‘𝑈)‘𝑋) = (𝐴‘𝑋)) |
46 | | eqid 2610 |
. . . . . . 7
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
47 | 19 | mplring 19273 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝐻 ∈ Ring) → 𝑈 ∈ Ring) |
48 | 19 | mpllmod 19272 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝐻 ∈ Ring) → 𝑈 ∈ LMod) |
49 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
50 | 41, 46, 47, 48, 49, 20 | asclf 19158 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ 𝐻 ∈ Ring) → (algSc‘𝑈):(Base‘(Scalar‘𝑈))⟶𝐵) |
51 | 1, 23, 50 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (algSc‘𝑈):(Base‘(Scalar‘𝑈))⟶𝐵) |
52 | 51 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → (algSc‘𝑈):(Base‘(Scalar‘𝑈))⟶𝐵) |
53 | 19, 1, 23 | mplsca 19266 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (Scalar‘𝑈)) |
54 | 53 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝐻) =
(Base‘(Scalar‘𝑈))) |
55 | 38, 54 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → 𝑇 = (Base‘(Scalar‘𝑈))) |
56 | 55 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ 𝑇 ↔ 𝑋 ∈ (Base‘(Scalar‘𝑈)))) |
57 | 56 | biimpa 500 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → 𝑋 ∈ (Base‘(Scalar‘𝑈))) |
58 | 52, 57 | ffvelrnd 6268 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → ((algSc‘𝑈)‘𝑋) ∈ 𝐵) |
59 | 45, 58 | eqeltrrd 2689 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → (𝐴‘𝑋) ∈ 𝐵) |
60 | 40, 59 | impbida 873 |
1
⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇)) |