| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqidd 2737 | . . . 4
⊢ (𝜑 → (𝐻 “s 𝑃) = (𝐻 “s 𝑃)) | 
| 2 |  | algextdeglem.u | . . . . 5
⊢ 𝑈 = (Base‘𝑃) | 
| 3 | 2 | a1i 11 | . . . 4
⊢ (𝜑 → 𝑈 = (Base‘𝑃)) | 
| 4 |  | algextdeg.e | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) | 
| 5 |  | algextdeg.k | . . . . . . . . . . . 12
⊢ 𝐾 = (𝐸 ↾s 𝐹) | 
| 6 | 5 | sdrgdrng 20792 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing) | 
| 7 | 4, 6 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ DivRing) | 
| 8 | 7 | drngringd 20738 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Ring) | 
| 9 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐾 ∈ Ring) | 
| 10 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈) | 
| 11 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0g‘(Poly1‘𝐸)) =
(0g‘(Poly1‘𝐸)) | 
| 12 |  | algextdeg.f | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ Field) | 
| 13 |  | algextdeg.m | . . . . . . . . . . 11
⊢ 𝑀 = (𝐸 minPoly 𝐹) | 
| 14 |  | algextdeg.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) | 
| 15 | 5 | fveq2i 6908 | . . . . . . . . . . 11
⊢
(Monic1p‘𝐾) = (Monic1p‘(𝐸 ↾s 𝐹)) | 
| 16 | 11, 12, 4, 13, 14, 15 | minplym1p 33757 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐴) ∈ (Monic1p‘𝐾)) | 
| 17 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑀‘𝐴) ∈ (Monic1p‘𝐾)) | 
| 18 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Unic1p‘𝐾) = (Unic1p‘𝐾) | 
| 19 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Monic1p‘𝐾) = (Monic1p‘𝐾) | 
| 20 | 18, 19 | mon1puc1p 26191 | . . . . . . . . 9
⊢ ((𝐾 ∈ Ring ∧ (𝑀‘𝐴) ∈ (Monic1p‘𝐾)) → (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) | 
| 21 | 9, 17, 20 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) | 
| 22 |  | algextdeglem.r | . . . . . . . . 9
⊢ 𝑅 = (rem1p‘𝐾) | 
| 23 |  | algextdeglem.y | . . . . . . . . 9
⊢ 𝑃 = (Poly1‘𝐾) | 
| 24 | 22, 23, 2, 18 | r1pcl 26199 | . . . . . . . 8
⊢ ((𝐾 ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈) | 
| 25 | 9, 10, 21, 24 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈) | 
| 26 |  | eqid 2736 | . . . . . . . . . 10
⊢
(deg1‘𝐾) = (deg1‘𝐾) | 
| 27 | 22, 23, 2, 18, 26 | r1pdeglt 26200 | . . . . . . . . 9
⊢ ((𝐾 ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) →
((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < ((deg1‘𝐾)‘(𝑀‘𝐴))) | 
| 28 | 9, 10, 21, 27 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < ((deg1‘𝐾)‘(𝑀‘𝐴))) | 
| 29 |  | algextdeg.d | . . . . . . . . . 10
⊢ 𝐷 = (deg1‘𝐸) | 
| 30 |  | algextdeglem.o | . . . . . . . . . . . 12
⊢ 𝑂 = (𝐸 evalSub1 𝐹) | 
| 31 | 5 | fveq2i 6908 | . . . . . . . . . . . . 13
⊢
(Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹)) | 
| 32 | 23, 31 | eqtri 2764 | . . . . . . . . . . . 12
⊢ 𝑃 =
(Poly1‘(𝐸
↾s 𝐹)) | 
| 33 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Base‘𝐸) =
(Base‘𝐸) | 
| 34 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(0g‘𝐸) = (0g‘𝐸) | 
| 35 | 12 | fldcrngd 20743 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ CRing) | 
| 36 |  | sdrgsubrg 20793 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸)) | 
| 37 | 4, 36 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) | 
| 38 | 30, 5, 33, 34, 35, 37 | irngssv 33739 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸)) | 
| 39 | 38, 14 | sseldd 3983 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸)) | 
| 40 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ {𝑝 ∈ dom 𝑂 ∣ ((𝑂‘𝑝)‘𝐴) = (0g‘𝐸)} = {𝑝 ∈ dom 𝑂 ∣ ((𝑂‘𝑝)‘𝐴) = (0g‘𝐸)} | 
| 41 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(RSpan‘𝑃) =
(RSpan‘𝑃) | 
| 42 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹)) | 
| 43 | 30, 32, 33, 12, 4, 39, 34, 40, 41, 42, 13 | minplycl 33750 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘𝑃)) | 
| 44 | 43, 2 | eleqtrrdi 2851 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈) | 
| 45 | 5, 29, 23, 2, 44, 37 | ressdeg1 33592 | . . . . . . . . 9
⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) = ((deg1‘𝐾)‘(𝑀‘𝐴))) | 
| 46 | 45 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝐷‘(𝑀‘𝐴)) = ((deg1‘𝐾)‘(𝑀‘𝐴))) | 
| 47 | 28, 46 | breqtrrd 5170 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴))) | 
| 48 |  | algextdeglem.t | . . . . . . . . 9
⊢ 𝑇 = (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) | 
| 49 | 12 | flddrngd 20742 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ DivRing) | 
| 50 | 49 | drngringd 20738 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ Ring) | 
| 51 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(Poly1‘𝐸) = (Poly1‘𝐸) | 
| 52 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(PwSer1‘𝐾) = (PwSer1‘𝐾) | 
| 53 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(Base‘(PwSer1‘𝐾)) =
(Base‘(PwSer1‘𝐾)) | 
| 54 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(Base‘(Poly1‘𝐸)) =
(Base‘(Poly1‘𝐸)) | 
| 55 | 51, 5, 23, 2, 37, 52, 53, 54 | ressply1bas2 22230 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 =
((Base‘(PwSer1‘𝐾)) ∩
(Base‘(Poly1‘𝐸)))) | 
| 56 |  | inss2 4237 | . . . . . . . . . . . 12
⊢
((Base‘(PwSer1‘𝐾)) ∩
(Base‘(Poly1‘𝐸))) ⊆
(Base‘(Poly1‘𝐸)) | 
| 57 | 55, 56 | eqsstrdi 4027 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆
(Base‘(Poly1‘𝐸))) | 
| 58 | 57, 44 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐴) ∈
(Base‘(Poly1‘𝐸))) | 
| 59 | 11, 12, 4, 13, 14 | irngnminplynz 33756 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐴) ≠
(0g‘(Poly1‘𝐸))) | 
| 60 | 29, 51, 11, 54 | deg1nn0cl 26128 | . . . . . . . . . 10
⊢ ((𝐸 ∈ Ring ∧ (𝑀‘𝐴) ∈
(Base‘(Poly1‘𝐸)) ∧ (𝑀‘𝐴) ≠
(0g‘(Poly1‘𝐸))) → (𝐷‘(𝑀‘𝐴)) ∈
ℕ0) | 
| 61 | 50, 58, 59, 60 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈
ℕ0) | 
| 62 | 23, 26, 48, 61, 8, 2 | ply1degleel 33617 | . . . . . . . 8
⊢ (𝜑 → ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ↔ ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈 ∧ ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴))))) | 
| 63 | 62 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ↔ ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈 ∧ ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴))))) | 
| 64 | 25, 47, 63 | mpbir2and 713 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇) | 
| 65 | 64 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑝 ∈ 𝑈 (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇) | 
| 66 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑝 = 𝑞 → (𝑝𝑅(𝑀‘𝐴)) = (𝑞𝑅(𝑀‘𝐴))) | 
| 67 | 66 | eqeq2d 2747 | . . . . . . . 8
⊢ (𝑝 = 𝑞 → (𝑞 = (𝑝𝑅(𝑀‘𝐴)) ↔ 𝑞 = (𝑞𝑅(𝑀‘𝐴)))) | 
| 68 |  | eqcom 2743 | . . . . . . . 8
⊢ (𝑞 = (𝑞𝑅(𝑀‘𝐴)) ↔ (𝑞𝑅(𝑀‘𝐴)) = 𝑞) | 
| 69 | 67, 68 | bitrdi 287 | . . . . . . 7
⊢ (𝑝 = 𝑞 → (𝑞 = (𝑝𝑅(𝑀‘𝐴)) ↔ (𝑞𝑅(𝑀‘𝐴)) = 𝑞)) | 
| 70 | 23, 26, 48, 61, 8, 2 | ply1degltel 33616 | . . . . . . . 8
⊢ (𝜑 → (𝑞 ∈ 𝑇 ↔ (𝑞 ∈ 𝑈 ∧ ((deg1‘𝐾)‘𝑞) ≤ ((𝐷‘(𝑀‘𝐴)) − 1)))) | 
| 71 | 70 | simprbda 498 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → 𝑞 ∈ 𝑈) | 
| 72 | 70 | simplbda 499 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) ≤ ((𝐷‘(𝑀‘𝐴)) − 1)) | 
| 73 | 45 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐷‘(𝑀‘𝐴)) − 1) =
(((deg1‘𝐾)‘(𝑀‘𝐴)) − 1)) | 
| 74 | 73 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((𝐷‘(𝑀‘𝐴)) − 1) =
(((deg1‘𝐾)‘(𝑀‘𝐴)) − 1)) | 
| 75 | 72, 74 | breqtrd 5168 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) ≤ (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1)) | 
| 76 | 26, 23, 2 | deg1cl 26123 | . . . . . . . . . . 11
⊢ (𝑞 ∈ 𝑈 → ((deg1‘𝐾)‘𝑞) ∈ (ℕ0 ∪
{-∞})) | 
| 77 | 71, 76 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) ∈ (ℕ0 ∪
{-∞})) | 
| 78 | 61 | nn0zd 12641 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈ ℤ) | 
| 79 | 45, 78 | eqeltrrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 →
((deg1‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ) | 
| 80 | 79 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ) | 
| 81 |  | degltlem1 26112 | . . . . . . . . . 10
⊢
((((deg1‘𝐾)‘𝑞) ∈ (ℕ0 ∪
{-∞}) ∧ ((deg1‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ) →
(((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴)) ↔ ((deg1‘𝐾)‘𝑞) ≤ (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1))) | 
| 82 | 77, 80, 81 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴)) ↔ ((deg1‘𝐾)‘𝑞) ≤ (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1))) | 
| 83 | 75, 82 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴))) | 
| 84 |  | fldsdrgfld 20800 | . . . . . . . . . . . . . 14
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field) | 
| 85 | 12, 4, 84 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field) | 
| 86 | 5, 85 | eqeltrid 2844 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ Field) | 
| 87 |  | fldidom 20772 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn) | 
| 88 | 86, 87 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ IDomn) | 
| 89 | 88 | idomdomd 20727 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ Domn) | 
| 90 | 89 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → 𝐾 ∈ Domn) | 
| 91 | 8, 16, 20 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) | 
| 92 | 91 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) | 
| 93 | 23, 2, 18, 22, 26, 90, 71, 92 | r1pid2 26202 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((𝑞𝑅(𝑀‘𝐴)) = 𝑞 ↔ ((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴)))) | 
| 94 | 83, 93 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (𝑞𝑅(𝑀‘𝐴)) = 𝑞) | 
| 95 | 69, 71, 94 | rspcedvdw 3624 | . . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴))) | 
| 96 | 95 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑞 ∈ 𝑇 ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴))) | 
| 97 |  | algextdeglem.h | . . . . . 6
⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴))) | 
| 98 | 97 | fompt 7137 | . . . . 5
⊢ (𝐻:𝑈–onto→𝑇 ↔ (∀𝑝 ∈ 𝑈 (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ∧ ∀𝑞 ∈ 𝑇 ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴)))) | 
| 99 | 65, 96, 98 | sylanbrc 583 | . . . 4
⊢ (𝜑 → 𝐻:𝑈–onto→𝑇) | 
| 100 | 23 | ply1ring 22250 | . . . . 5
⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring) | 
| 101 | 8, 100 | syl 17 | . . . 4
⊢ (𝜑 → 𝑃 ∈ Ring) | 
| 102 | 1, 3, 99, 101 | imasbas 17558 | . . 3
⊢ (𝜑 → 𝑇 = (Base‘(𝐻 “s 𝑃))) | 
| 103 | 71 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑞 ∈ 𝑇 → 𝑞 ∈ 𝑈)) | 
| 104 | 103 | ssrdv 3988 | . . . 4
⊢ (𝜑 → 𝑇 ⊆ 𝑈) | 
| 105 |  | eqid 2736 | . . . . 5
⊢ (𝑃 ↾s 𝑇) = (𝑃 ↾s 𝑇) | 
| 106 | 105, 2 | ressbas2 17284 | . . . 4
⊢ (𝑇 ⊆ 𝑈 → 𝑇 = (Base‘(𝑃 ↾s 𝑇))) | 
| 107 | 104, 106 | syl 17 | . . 3
⊢ (𝜑 → 𝑇 = (Base‘(𝑃 ↾s 𝑇))) | 
| 108 |  | ssidd 4006 | . . 3
⊢ (𝜑 → 𝑇 ⊆ 𝑇) | 
| 109 |  | eqid 2736 | . . . . . . 7
⊢ (𝐻 “s
𝑃) = (𝐻 “s 𝑃) | 
| 110 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘(𝐻
“s 𝑃)) = (Base‘(𝐻 “s 𝑃)) | 
| 111 | 104 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑇 ⊆ 𝑈) | 
| 112 |  | simplr 768 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑥 ∈ 𝑇) | 
| 113 | 111, 112 | sseldd 3983 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑥 ∈ 𝑈) | 
| 114 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑇) | 
| 115 | 111, 114 | sseldd 3983 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑈) | 
| 116 |  | foeq3 6817 | . . . . . . . . . 10
⊢ (𝑇 = (Base‘(𝐻 “s
𝑃)) → (𝐻:𝑈–onto→𝑇 ↔ 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃)))) | 
| 117 | 102, 116 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐻:𝑈–onto→𝑇 ↔ 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃)))) | 
| 118 | 99, 117 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃))) | 
| 119 | 118 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃))) | 
| 120 | 23, 2, 22, 18, 97, 8, 91 | r1plmhm 33631 | . . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ (𝑃 LMHom (𝐻 “s 𝑃))) | 
| 121 | 120 | lmhmghmd 33043 | . . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ (𝑃 GrpHom (𝐻 “s 𝑃))) | 
| 122 |  | ghmmhm 19245 | . . . . . . . . 9
⊢ (𝐻 ∈ (𝑃 GrpHom (𝐻 “s 𝑃)) → 𝐻 ∈ (𝑃 MndHom (𝐻 “s 𝑃))) | 
| 123 | 121, 122 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ (𝑃 MndHom (𝐻 “s 𝑃))) | 
| 124 | 123 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐻 ∈ (𝑃 MndHom (𝐻 “s 𝑃))) | 
| 125 |  | eqid 2736 | . . . . . . 7
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 126 |  | eqid 2736 | . . . . . . 7
⊢
(+g‘(𝐻 “s 𝑃)) = (+g‘(𝐻 “s
𝑃)) | 
| 127 | 109, 2, 110, 113, 115, 119, 124, 125, 126 | mhmimasplusg 33044 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝐻‘𝑥)(+g‘(𝐻 “s 𝑃))(𝐻‘𝑦)) = (𝐻‘(𝑥(+g‘𝑃)𝑦))) | 
| 128 |  | algextdeg.l | . . . . . . . . 9
⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) | 
| 129 | 12 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐸 ∈ Field) | 
| 130 | 4 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐹 ∈ (SubDRing‘𝐸)) | 
| 131 | 14 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐴 ∈ (𝐸 IntgRing 𝐹)) | 
| 132 |  | algextdeglem.g | . . . . . . . . 9
⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) | 
| 133 |  | algextdeglem.n | . . . . . . . . 9
⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) | 
| 134 |  | algextdeglem.z | . . . . . . . . 9
⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) | 
| 135 |  | algextdeglem.q | . . . . . . . . 9
⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) | 
| 136 |  | algextdeglem.j | . . . . . . . . 9
⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪
(𝐺 “ 𝑝)) | 
| 137 | 5, 128, 29, 13, 129, 130, 131, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 113 | algextdeglem7 33765 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥 ∈ 𝑇 ↔ (𝐻‘𝑥) = 𝑥)) | 
| 138 | 112, 137 | mpbid 232 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘𝑥) = 𝑥) | 
| 139 | 5, 128, 29, 13, 129, 130, 131, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 115 | algextdeglem7 33765 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑦 ∈ 𝑇 ↔ (𝐻‘𝑦) = 𝑦)) | 
| 140 | 114, 139 | mpbid 232 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘𝑦) = 𝑦) | 
| 141 | 138, 140 | oveq12d 7450 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝐻‘𝑥)(+g‘(𝐻 “s 𝑃))(𝐻‘𝑦)) = (𝑥(+g‘(𝐻 “s 𝑃))𝑦)) | 
| 142 | 101 | ringgrpd 20240 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ Grp) | 
| 143 | 23, 7 | ply1lvec 33586 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ LVec) | 
| 144 | 23, 26, 48, 61, 8 | ply1degltlss 33618 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ (LSubSp‘𝑃)) | 
| 145 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(LSubSp‘𝑃) =
(LSubSp‘𝑃) | 
| 146 | 105, 145 | lsslvec 21109 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ LVec ∧ 𝑇 ∈ (LSubSp‘𝑃)) → (𝑃 ↾s 𝑇) ∈ LVec) | 
| 147 | 143, 144,
146 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃 ↾s 𝑇) ∈ LVec) | 
| 148 | 147 | lvecgrpd 21108 | . . . . . . . . . 10
⊢ (𝜑 → (𝑃 ↾s 𝑇) ∈ Grp) | 
| 149 | 2 | issubg 19145 | . . . . . . . . . 10
⊢ (𝑇 ∈ (SubGrp‘𝑃) ↔ (𝑃 ∈ Grp ∧ 𝑇 ⊆ 𝑈 ∧ (𝑃 ↾s 𝑇) ∈ Grp)) | 
| 150 | 142, 104,
148, 149 | syl3anbrc 1343 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝑃)) | 
| 151 | 150 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑇 ∈ (SubGrp‘𝑃)) | 
| 152 | 125 | subgcl 19155 | . . . . . . . 8
⊢ ((𝑇 ∈ (SubGrp‘𝑃) ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘𝑃)𝑦) ∈ 𝑇) | 
| 153 | 151, 112,
114, 152 | syl3anc 1372 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘𝑃)𝑦) ∈ 𝑇) | 
| 154 | 142 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑃 ∈ Grp) | 
| 155 | 2, 125, 154, 113, 115 | grpcld 18966 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘𝑃)𝑦) ∈ 𝑈) | 
| 156 | 5, 128, 29, 13, 129, 130, 131, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 155 | algextdeglem7 33765 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝑥(+g‘𝑃)𝑦) ∈ 𝑇 ↔ (𝐻‘(𝑥(+g‘𝑃)𝑦)) = (𝑥(+g‘𝑃)𝑦))) | 
| 157 | 153, 156 | mpbid 232 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘(𝑥(+g‘𝑃)𝑦)) = (𝑥(+g‘𝑃)𝑦)) | 
| 158 | 127, 141,
157 | 3eqtr3d 2784 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘(𝐻 “s 𝑃))𝑦) = (𝑥(+g‘𝑃)𝑦)) | 
| 159 |  | fvex 6918 | . . . . . . . . 9
⊢
(deg1‘𝐾) ∈ V | 
| 160 |  | cnvexg 7947 | . . . . . . . . 9
⊢
((deg1‘𝐾) ∈ V → ◡(deg1‘𝐾) ∈ V) | 
| 161 |  | imaexg 7936 | . . . . . . . . 9
⊢ (◡(deg1‘𝐾) ∈ V → (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) ∈ V) | 
| 162 | 159, 160,
161 | mp2b 10 | . . . . . . . 8
⊢ (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) ∈ V | 
| 163 | 48, 162 | eqeltri 2836 | . . . . . . 7
⊢ 𝑇 ∈ V | 
| 164 | 105, 125 | ressplusg 17335 | . . . . . . 7
⊢ (𝑇 ∈ V →
(+g‘𝑃) =
(+g‘(𝑃
↾s 𝑇))) | 
| 165 | 163, 164 | ax-mp 5 | . . . . . 6
⊢
(+g‘𝑃) = (+g‘(𝑃 ↾s 𝑇)) | 
| 166 | 165 | oveqi 7445 | . . . . 5
⊢ (𝑥(+g‘𝑃)𝑦) = (𝑥(+g‘(𝑃 ↾s 𝑇))𝑦) | 
| 167 | 158, 166 | eqtrdi 2792 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘(𝐻 “s 𝑃))𝑦) = (𝑥(+g‘(𝑃 ↾s 𝑇))𝑦)) | 
| 168 | 167 | anasss 466 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥(+g‘(𝐻 “s 𝑃))𝑦) = (𝑥(+g‘(𝑃 ↾s 𝑇))𝑦)) | 
| 169 |  | simprr 772 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑦 ∈ 𝑇) | 
| 170 | 12 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐸 ∈ Field) | 
| 171 | 4 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐹 ∈ (SubDRing‘𝐸)) | 
| 172 | 14 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐴 ∈ (𝐸 IntgRing 𝐹)) | 
| 173 | 104 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑇 ⊆ 𝑈) | 
| 174 | 173, 169 | sseldd 3983 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑦 ∈ 𝑈) | 
| 175 | 5, 128, 29, 13, 170, 171, 172, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 174 | algextdeglem7 33765 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑦 ∈ 𝑇 ↔ (𝐻‘𝑦) = 𝑦)) | 
| 176 | 169, 175 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘𝑦) = 𝑦) | 
| 177 | 176 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘(𝐻
“s 𝑃))(𝐻‘𝑦)) = (𝑥( ·𝑠
‘(𝐻
“s 𝑃))𝑦)) | 
| 178 |  | simprl 770 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑥 ∈ 𝐹) | 
| 179 | 33 | sdrgss 20795 | . . . . . . . . . 10
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ (Base‘𝐸)) | 
| 180 | 5, 33 | ressbas2 17284 | . . . . . . . . . 10
⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾)) | 
| 181 | 4, 179, 180 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 = (Base‘𝐾)) | 
| 182 | 23 | ply1sca 22255 | . . . . . . . . . . 11
⊢ (𝐾 ∈ Ring → 𝐾 = (Scalar‘𝑃)) | 
| 183 | 8, 182 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 = (Scalar‘𝑃)) | 
| 184 | 183 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(Scalar‘𝑃))) | 
| 185 | 181, 184 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → 𝐹 = (Base‘(Scalar‘𝑃))) | 
| 186 | 185 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐹 = (Base‘(Scalar‘𝑃))) | 
| 187 | 178, 186 | eleqtrd 2842 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑥 ∈ (Base‘(Scalar‘𝑃))) | 
| 188 | 118 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃))) | 
| 189 | 120 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻 ∈ (𝑃 LMHom (𝐻 “s 𝑃))) | 
| 190 |  | eqid 2736 | . . . . . 6
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) | 
| 191 |  | eqid 2736 | . . . . . 6
⊢ (
·𝑠 ‘(𝐻 “s 𝑃)) = (
·𝑠 ‘(𝐻 “s 𝑃)) | 
| 192 |  | eqid 2736 | . . . . . 6
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) | 
| 193 | 109, 2, 110, 187, 174, 188, 189, 190, 191, 192 | lmhmimasvsca 33045 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘(𝐻
“s 𝑃))(𝐻‘𝑦)) = (𝐻‘(𝑥( ·𝑠
‘𝑃)𝑦))) | 
| 194 | 177, 193 | eqtr3d 2778 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘(𝐻
“s 𝑃))𝑦) = (𝐻‘(𝑥( ·𝑠
‘𝑃)𝑦))) | 
| 195 | 64, 97 | fmptd 7133 | . . . . . 6
⊢ (𝜑 → 𝐻:𝑈⟶𝑇) | 
| 196 | 195 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻:𝑈⟶𝑇) | 
| 197 |  | eqid 2736 | . . . . . 6
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) | 
| 198 | 143 | lveclmodd 21107 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ LMod) | 
| 199 | 198 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑃 ∈ LMod) | 
| 200 | 2, 197, 190, 192, 199, 187, 174 | lmodvscld 20878 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘𝑃)𝑦) ∈ 𝑈) | 
| 201 | 196, 200 | ffvelcdmd 7104 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘(𝑥( ·𝑠
‘𝑃)𝑦)) ∈ 𝑇) | 
| 202 | 194, 201 | eqeltrd 2840 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘(𝐻
“s 𝑃))𝑦) ∈ 𝑇) | 
| 203 | 144 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑇 ∈ (LSubSp‘𝑃)) | 
| 204 | 197, 190,
192, 145 | lssvscl 20954 | . . . . . 6
⊢ (((𝑃 ∈ LMod ∧ 𝑇 ∈ (LSubSp‘𝑃)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘𝑃)𝑦) ∈ 𝑇) | 
| 205 | 199, 203,
187, 169, 204 | syl22anc 838 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘𝑃)𝑦) ∈ 𝑇) | 
| 206 | 5, 128, 29, 13, 170, 171, 172, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 200 | algextdeglem7 33765 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → ((𝑥( ·𝑠
‘𝑃)𝑦) ∈ 𝑇 ↔ (𝐻‘(𝑥( ·𝑠
‘𝑃)𝑦)) = (𝑥( ·𝑠
‘𝑃)𝑦))) | 
| 207 | 205, 206 | mpbid 232 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘(𝑥( ·𝑠
‘𝑃)𝑦)) = (𝑥( ·𝑠
‘𝑃)𝑦)) | 
| 208 | 105, 190 | ressvsca 17389 | . . . . . 6
⊢ (𝑇 ∈ V → (
·𝑠 ‘𝑃) = ( ·𝑠
‘(𝑃
↾s 𝑇))) | 
| 209 | 163, 208 | mp1i 13 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (
·𝑠 ‘𝑃) = ( ·𝑠
‘(𝑃
↾s 𝑇))) | 
| 210 | 209 | oveqd 7449 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘𝑃)𝑦) = (𝑥( ·𝑠
‘(𝑃
↾s 𝑇))𝑦)) | 
| 211 | 194, 207,
210 | 3eqtrd 2780 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠
‘(𝐻
“s 𝑃))𝑦) = (𝑥( ·𝑠
‘(𝑃
↾s 𝑇))𝑦)) | 
| 212 |  | eqid 2736 | . . 3
⊢
(Scalar‘(𝐻
“s 𝑃)) = (Scalar‘(𝐻 “s 𝑃)) | 
| 213 | 105, 197 | resssca 17388 | . . . 4
⊢ (𝑇 ∈ V →
(Scalar‘𝑃) =
(Scalar‘(𝑃
↾s 𝑇))) | 
| 214 | 163, 213 | ax-mp 5 | . . 3
⊢
(Scalar‘𝑃) =
(Scalar‘(𝑃
↾s 𝑇)) | 
| 215 | 1, 3, 99, 101, 197 | imassca 17565 | . . . . . 6
⊢ (𝜑 → (Scalar‘𝑃) = (Scalar‘(𝐻 “s
𝑃))) | 
| 216 | 183, 215 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → 𝐾 = (Scalar‘(𝐻 “s 𝑃))) | 
| 217 | 216 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(Scalar‘(𝐻 “s 𝑃)))) | 
| 218 | 181, 217 | eqtrd 2776 | . . 3
⊢ (𝜑 → 𝐹 = (Base‘(Scalar‘(𝐻 “s
𝑃)))) | 
| 219 | 215 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 →
(+g‘(Scalar‘𝑃)) =
(+g‘(Scalar‘(𝐻 “s 𝑃)))) | 
| 220 | 219 | oveqd 7449 | . . . . 5
⊢ (𝜑 → (𝑥(+g‘(Scalar‘𝑃))𝑦) = (𝑥(+g‘(Scalar‘(𝐻 “s
𝑃)))𝑦)) | 
| 221 | 220 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (𝑥(+g‘(Scalar‘(𝐻 “s
𝑃)))𝑦) = (𝑥(+g‘(Scalar‘𝑃))𝑦)) | 
| 222 | 221 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥(+g‘(Scalar‘(𝐻 “s
𝑃)))𝑦) = (𝑥(+g‘(Scalar‘𝑃))𝑦)) | 
| 223 |  | lmhmlvec2 33671 | . . . 4
⊢ ((𝑃 ∈ LVec ∧ 𝐻 ∈ (𝑃 LMHom (𝐻 “s 𝑃))) → (𝐻 “s 𝑃) ∈ LVec) | 
| 224 | 143, 120,
223 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐻 “s 𝑃) ∈ LVec) | 
| 225 | 102, 107,
108, 168, 202, 211, 212, 214, 218, 185, 222, 224, 147 | dimpropd 33660 | . 2
⊢ (𝜑 → (dim‘(𝐻 “s
𝑃)) = (dim‘(𝑃 ↾s 𝑇))) | 
| 226 | 23, 26, 48, 61, 7, 105 | ply1degltdim 33675 | . 2
⊢ (𝜑 → (dim‘(𝑃 ↾s 𝑇)) = (𝐷‘(𝑀‘𝐴))) | 
| 227 | 225, 226 | eqtrd 2776 | 1
⊢ (𝜑 → (dim‘(𝐻 “s
𝑃)) = (𝐷‘(𝑀‘𝐴))) |