| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
| 2 | | mplind.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
| 3 | | mplind.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 4 | 1, 2, 3 | psrassa 21993 |
. . . . 5
⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg) |
| 5 | | inss2 4238 |
. . . . . 6
⊢ (𝐻 ∩ 𝐵) ⊆ 𝐵 |
| 6 | | mplind.sy |
. . . . . . . 8
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
| 7 | | mplind.sb |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
| 8 | | crngring 20242 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 9 | 3, 8 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 10 | 1, 6, 7, 2, 9 | mplsubrg 22025 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
| 12 | 11 | subrgss 20572 |
. . . . . . 7
⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
| 13 | 10, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
| 14 | 5, 13 | sstrid 3995 |
. . . . 5
⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
| 15 | | mplind.sv |
. . . . . . . . 9
⊢ 𝑉 = (𝐼 mVar 𝑅) |
| 16 | 6, 15, 7, 2, 9 | mvrf2 22013 |
. . . . . . . 8
⊢ (𝜑 → 𝑉:𝐼⟶𝐵) |
| 17 | 16 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝑉 Fn 𝐼) |
| 18 | | mplind.v |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻) |
| 19 | 18 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻) |
| 20 | | fnfvrnss 7141 |
. . . . . . 7
⊢ ((𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻) → ran 𝑉 ⊆ 𝐻) |
| 21 | 17, 19, 20 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ran 𝑉 ⊆ 𝐻) |
| 22 | 16 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran 𝑉 ⊆ 𝐵) |
| 23 | 21, 22 | ssind 4241 |
. . . . 5
⊢ (𝜑 → ran 𝑉 ⊆ (𝐻 ∩ 𝐵)) |
| 24 | | eqid 2737 |
. . . . . 6
⊢
(AlgSpan‘(𝐼
mPwSer 𝑅)) =
(AlgSpan‘(𝐼 mPwSer
𝑅)) |
| 25 | 24, 11 | aspss 21897 |
. . . . 5
⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ (𝐻 ∩ 𝐵) ⊆ (Base‘(𝐼 mPwSer 𝑅)) ∧ ran 𝑉 ⊆ (𝐻 ∩ 𝐵)) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) ⊆ ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵))) |
| 26 | 4, 14, 23, 25 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) ⊆ ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵))) |
| 27 | 6, 1, 15, 24, 2, 3 | mplbas2 22060 |
. . . . 5
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑌)) |
| 28 | 27, 7 | eqtr4di 2795 |
. . . 4
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = 𝐵) |
| 29 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ 𝐵) |
| 30 | 6 | mplassa 22042 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑌 ∈ AssAlg) |
| 31 | 2, 3, 30 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ AssAlg) |
| 32 | | mplind.sc |
. . . . . . . . . . . . . 14
⊢ 𝐶 = (algSc‘𝑌) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
| 34 | 32, 33 | asclrhm 21910 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ AssAlg → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌)) |
| 35 | 31, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌)) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1r‘(Scalar‘𝑌)) =
(1r‘(Scalar‘𝑌)) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑌) = (1r‘𝑌) |
| 38 | 36, 37 | rhm1 20489 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → (𝐶‘(1r‘(Scalar‘𝑌))) = (1r‘𝑌)) |
| 39 | 35, 38 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘(1r‘(Scalar‘𝑌))) = (1r‘𝑌)) |
| 40 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 =
(1r‘(Scalar‘𝑌)) → (𝐶‘𝑥) = (𝐶‘(1r‘(Scalar‘𝑌)))) |
| 41 | 40 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑥 =
(1r‘(Scalar‘𝑌)) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘(1r‘(Scalar‘𝑌))) ∈ 𝐻)) |
| 42 | | mplind.s |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻) |
| 43 | 42 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻) |
| 44 | 6, 2, 3 | mplsca 22033 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 = (Scalar‘𝑌)) |
| 45 | 44, 9 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Scalar‘𝑌) ∈ Ring) |
| 46 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
| 47 | 46, 36 | ringidcl 20262 |
. . . . . . . . . . . . . 14
⊢
((Scalar‘𝑌)
∈ Ring → (1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) |
| 48 | 45, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) |
| 49 | | mplind.sk |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (Base‘𝑅) |
| 50 | 44 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑌))) |
| 51 | 49, 50 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑌))) |
| 52 | 48, 51 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(1r‘(Scalar‘𝑌)) ∈ 𝐾) |
| 53 | 41, 43, 52 | rspcdva 3623 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘(1r‘(Scalar‘𝑌))) ∈ 𝐻) |
| 54 | 39, 53 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑌) ∈ 𝐻) |
| 55 | | assaring 21881 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ Ring) |
| 56 | 31, 55 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Ring) |
| 57 | 7, 37 | ringidcl 20262 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Ring →
(1r‘𝑌)
∈ 𝐵) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑌) ∈ 𝐵) |
| 59 | 54, 58 | elind 4200 |
. . . . . . . . 9
⊢ (𝜑 → (1r‘𝑌) ∈ (𝐻 ∩ 𝐵)) |
| 60 | 59 | ne0d 4342 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 ∩ 𝐵) ≠ ∅) |
| 61 | | elinel1 4201 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐻 ∩ 𝐵) → 𝑧 ∈ 𝐻) |
| 62 | | elinel1 4201 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝐻 ∩ 𝐵) → 𝑤 ∈ 𝐻) |
| 63 | 61, 62 | anim12i 613 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) |
| 64 | | mplind.p |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻) |
| 65 | 64 | caovclg 7625 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → (𝑧 + 𝑤) ∈ 𝐻) |
| 66 | 63, 65 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐻) |
| 67 | | assalmod 21880 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ LMod) |
| 68 | 31, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ LMod) |
| 69 | | lmodgrp 20865 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ LMod → 𝑌 ∈ Grp) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ Grp) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Grp) |
| 72 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (𝐻 ∩ 𝐵)) |
| 73 | 72 | elin2d 4205 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐵) |
| 74 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵)) |
| 75 | 74 | elin2d 4205 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵) |
| 76 | | mplind.sp |
. . . . . . . . . . . . . . 15
⊢ + =
(+g‘𝑌) |
| 77 | 7, 76 | grpcl 18959 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵) |
| 78 | 71, 73, 75, 77 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐵) |
| 79 | 66, 78 | elind 4200 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵)) |
| 80 | 79 | anassrs 467 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵)) |
| 81 | 80 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵)) |
| 82 | | mplind.st |
. . . . . . . . . . . . 13
⊢ · =
(.r‘𝑌) |
| 83 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(invg‘𝑌) = (invg‘𝑌) |
| 84 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Ring) |
| 85 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ (𝐻 ∩ 𝐵)) |
| 86 | 85 | elin2d 4205 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐵) |
| 87 | 7, 82, 37, 83, 84, 86 | ringnegl 20299 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((invg‘𝑌)‘(1r‘𝑌)) · 𝑧) = ((invg‘𝑌)‘𝑧)) |
| 88 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝜑) |
| 89 | | rhmghm 20484 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌)) |
| 90 | 35, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌)) |
| 91 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(invg‘(Scalar‘𝑌)) =
(invg‘(Scalar‘𝑌)) |
| 92 | 46, 91, 83 | ghminv 19241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌) ∧
(1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) = ((invg‘𝑌)‘(𝐶‘(1r‘(Scalar‘𝑌))))) |
| 93 | 90, 48, 92 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) = ((invg‘𝑌)‘(𝐶‘(1r‘(Scalar‘𝑌))))) |
| 94 | 39 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
((invg‘𝑌)‘(𝐶‘(1r‘(Scalar‘𝑌)))) =
((invg‘𝑌)‘(1r‘𝑌))) |
| 95 | 93, 94 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) = ((invg‘𝑌)‘(1r‘𝑌))) |
| 96 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) → (𝐶‘𝑥) = (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))))) |
| 97 | 96 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 =
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) ∈ 𝐻)) |
| 98 | | ringgrp 20235 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Scalar‘𝑌)
∈ Ring → (Scalar‘𝑌) ∈ Grp) |
| 99 | 45, 98 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Scalar‘𝑌) ∈ Grp) |
| 100 | 46, 91 | grpinvcl 19005 |
. . . . . . . . . . . . . . . . . 18
⊢
(((Scalar‘𝑌)
∈ Grp ∧ (1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) →
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) ∈
(Base‘(Scalar‘𝑌))) |
| 101 | 99, 48, 100 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) ∈
(Base‘(Scalar‘𝑌))) |
| 102 | 101, 51 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) ∈ 𝐾) |
| 103 | 97, 43, 102 | rspcdva 3623 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) ∈ 𝐻) |
| 104 | 95, 103 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((invg‘𝑌)‘(1r‘𝑌)) ∈ 𝐻) |
| 105 | 104 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘(1r‘𝑌)) ∈ 𝐻) |
| 106 | 85 | elin1d 4204 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐻) |
| 107 | | mplind.t |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻) |
| 108 | 107 | caovclg 7625 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧
(((invg‘𝑌)‘(1r‘𝑌)) ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (((invg‘𝑌)‘(1r‘𝑌)) · 𝑧) ∈ 𝐻) |
| 109 | 88, 105, 106, 108 | syl12anc 837 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((invg‘𝑌)‘(1r‘𝑌)) · 𝑧) ∈ 𝐻) |
| 110 | 87, 109 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘𝑧) ∈ 𝐻) |
| 111 | 70 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Grp) |
| 112 | 7, 83 | grpinvcl 19005 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵) → ((invg‘𝑌)‘𝑧) ∈ 𝐵) |
| 113 | 111, 86, 112 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘𝑧) ∈ 𝐵) |
| 114 | 110, 113 | elind 4200 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)) |
| 115 | 81, 114 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))) |
| 116 | 115 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))) |
| 117 | 7, 76, 83 | issubg2 19159 |
. . . . . . . . 9
⊢ (𝑌 ∈ Grp → ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐻 ∩ 𝐵) ≠ ∅ ∧ ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))))) |
| 118 | 70, 117 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐻 ∩ 𝐵) ≠ ∅ ∧ ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))))) |
| 119 | 29, 60, 116, 118 | mpbir3and 1343 |
. . . . . . 7
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌)) |
| 120 | | elinel1 4201 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐻 ∩ 𝐵) → 𝑥 ∈ 𝐻) |
| 121 | | elinel1 4201 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐻 ∩ 𝐵) → 𝑦 ∈ 𝐻) |
| 122 | 120, 121 | anim12i 613 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵)) → (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) |
| 123 | 122, 107 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐻) |
| 124 | 56 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Ring) |
| 125 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ (𝐻 ∩ 𝐵)) |
| 126 | 125 | elin2d 4205 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ 𝐵) |
| 127 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ (𝐻 ∩ 𝐵)) |
| 128 | 127 | elin2d 4205 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ 𝐵) |
| 129 | 7, 82 | ringcl 20247 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
| 130 | 124, 126,
128, 129 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐵) |
| 131 | 123, 130 | elind 4200 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)) |
| 132 | 131 | ralrimivva 3202 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)) |
| 133 | 7, 37, 82 | issubrg2 20592 |
. . . . . . . 8
⊢ (𝑌 ∈ Ring → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ (1r‘𝑌) ∈ (𝐻 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)))) |
| 134 | 56, 133 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ (1r‘𝑌) ∈ (𝐻 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)))) |
| 135 | 119, 59, 132, 134 | mpbir3and 1343 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌)) |
| 136 | 6, 1, 7 | mplval2 22016 |
. . . . . . . 8
⊢ 𝑌 = ((𝐼 mPwSer 𝑅) ↾s 𝐵) |
| 137 | 136 | subsubrg 20598 |
. . . . . . 7
⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ⊆ 𝐵))) |
| 138 | 137 | simprbda 498 |
. . . . . 6
⊢ ((𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌)) → (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
| 139 | 10, 135, 138 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
| 140 | | assalmod 21880 |
. . . . . . 7
⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ LMod) |
| 141 | 4, 140 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ LMod) |
| 142 | 1, 6, 7, 2, 9 | mpllss 22023 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) |
| 143 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ AssAlg) |
| 144 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (Base‘(Scalar‘𝑌))) |
| 145 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵)) |
| 146 | 145 | elin2d 4205 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵) |
| 147 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
| 148 | 32, 33, 46, 7, 82, 147 | asclmul1 21906 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ AssAlg ∧ 𝑧 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·𝑠
‘𝑌)𝑤)) |
| 149 | 143, 144,
146, 148 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·𝑠
‘𝑌)𝑤)) |
| 150 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐶‘𝑥) = (𝐶‘𝑧)) |
| 151 | 150 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘𝑧) ∈ 𝐻)) |
| 152 | 43 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻) |
| 153 | 51 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝐾 = (Base‘(Scalar‘𝑌))) |
| 154 | 144, 153 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐾) |
| 155 | 151, 152,
154 | rspcdva 3623 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝐶‘𝑧) ∈ 𝐻) |
| 156 | 145 | elin1d 4204 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐻) |
| 157 | 155, 156 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) |
| 158 | 107 | caovclg 7625 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻) |
| 159 | 157, 158 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻) |
| 160 | 149, 159 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ 𝐻) |
| 161 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ LMod) |
| 162 | 7, 33, 147, 46 | lmodvscl 20876 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ LMod ∧ 𝑧 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ 𝐵) |
| 163 | 161, 144,
146, 162 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ 𝐵) |
| 164 | 160, 163 | elind 4200 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)) |
| 165 | 164 | ralrimivva 3202 |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)) |
| 166 | | eqid 2737 |
. . . . . . . . 9
⊢
(LSubSp‘𝑌) =
(LSubSp‘𝑌) |
| 167 | 33, 46, 7, 147, 166 | islss4 20960 |
. . . . . . . 8
⊢ (𝑌 ∈ LMod → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)))) |
| 168 | 68, 167 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)))) |
| 169 | 119, 165,
168 | mpbir2and 713 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌)) |
| 170 | | eqid 2737 |
. . . . . . . 8
⊢
(LSubSp‘(𝐼
mPwSer 𝑅)) =
(LSubSp‘(𝐼 mPwSer
𝑅)) |
| 171 | 136, 170,
166 | lsslss 20959 |
. . . . . . 7
⊢ (((𝐼 mPwSer 𝑅) ∈ LMod ∧ 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ⊆ 𝐵))) |
| 172 | 171 | simprbda 498 |
. . . . . 6
⊢ ((((𝐼 mPwSer 𝑅) ∈ LMod ∧ 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) ∧ (𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌)) → (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) |
| 173 | 141, 142,
169, 172 | syl21anc 838 |
. . . . 5
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) |
| 174 | 24, 11, 170 | aspid 21895 |
. . . . 5
⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵)) |
| 175 | 4, 139, 173, 174 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵)) |
| 176 | 26, 28, 175 | 3sstr3d 4038 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ (𝐻 ∩ 𝐵)) |
| 177 | | mplind.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 178 | 176, 177 | sseldd 3984 |
. 2
⊢ (𝜑 → 𝑋 ∈ (𝐻 ∩ 𝐵)) |
| 179 | 178 | elin1d 4204 |
1
⊢ (𝜑 → 𝑋 ∈ 𝐻) |