Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. 2
⊢ (𝐻 ∩ 𝐵) ⊆ 𝐻 |
2 | | eqid 2622 |
. . . . . 6
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
3 | | mplind.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ V) |
4 | | mplind.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CRing) |
5 | 2, 3, 4 | psrassa 19414 |
. . . . 5
⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg) |
6 | | inss2 3834 |
. . . . . 6
⊢ (𝐻 ∩ 𝐵) ⊆ 𝐵 |
7 | | mplind.sy |
. . . . . . . 8
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
8 | | mplind.sb |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
9 | | crngring 18558 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
10 | 4, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
11 | 2, 7, 8, 3, 10 | mplsubrg 19440 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
12 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
13 | 12 | subrgss 18781 |
. . . . . . 7
⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
14 | 11, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
15 | 6, 14 | syl5ss 3614 |
. . . . 5
⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
16 | | mplind.sv |
. . . . . . . . 9
⊢ 𝑉 = (𝐼 mVar 𝑅) |
17 | 7, 16, 8, 3, 10 | mvrf2 19492 |
. . . . . . . 8
⊢ (𝜑 → 𝑉:𝐼⟶𝐵) |
18 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑉:𝐼⟶𝐵 → 𝑉 Fn 𝐼) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑉 Fn 𝐼) |
20 | | mplind.v |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻) |
21 | 20 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻) |
22 | | fnfvrnss 6390 |
. . . . . . 7
⊢ ((𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻) → ran 𝑉 ⊆ 𝐻) |
23 | 19, 21, 22 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ran 𝑉 ⊆ 𝐻) |
24 | | frn 6053 |
. . . . . . 7
⊢ (𝑉:𝐼⟶𝐵 → ran 𝑉 ⊆ 𝐵) |
25 | 17, 24 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝑉 ⊆ 𝐵) |
26 | 23, 25 | ssind 3837 |
. . . . 5
⊢ (𝜑 → ran 𝑉 ⊆ (𝐻 ∩ 𝐵)) |
27 | | eqid 2622 |
. . . . . 6
⊢
(AlgSpan‘(𝐼
mPwSer 𝑅)) =
(AlgSpan‘(𝐼 mPwSer
𝑅)) |
28 | 27, 12 | aspss 19332 |
. . . . 5
⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ (𝐻 ∩ 𝐵) ⊆ (Base‘(𝐼 mPwSer 𝑅)) ∧ ran 𝑉 ⊆ (𝐻 ∩ 𝐵)) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) ⊆ ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵))) |
29 | 5, 15, 26, 28 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) ⊆ ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵))) |
30 | 7, 2, 16, 27, 3, 4 | mplbas2 19470 |
. . . . 5
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑌)) |
31 | 30, 8 | syl6eqr 2674 |
. . . 4
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = 𝐵) |
32 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ 𝐵) |
33 | 7 | mplassa 19454 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ CRing) → 𝑌 ∈ AssAlg) |
34 | 3, 4, 33 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ AssAlg) |
35 | | mplind.sc |
. . . . . . . . . . . . . 14
⊢ 𝐶 = (algSc‘𝑌) |
36 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
37 | 35, 36 | asclrhm 19342 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ AssAlg → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌)) |
38 | 34, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌)) |
39 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(1r‘(Scalar‘𝑌)) =
(1r‘(Scalar‘𝑌)) |
40 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑌) = (1r‘𝑌) |
41 | 39, 40 | rhm1 18730 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → (𝐶‘(1r‘(Scalar‘𝑌))) = (1r‘𝑌)) |
42 | 38, 41 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘(1r‘(Scalar‘𝑌))) = (1r‘𝑌)) |
43 | 7, 3, 4 | mplsca 19445 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 = (Scalar‘𝑌)) |
44 | 43, 10 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Scalar‘𝑌) ∈ Ring) |
45 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
46 | 45, 39 | ringidcl 18568 |
. . . . . . . . . . . . . 14
⊢
((Scalar‘𝑌)
∈ Ring → (1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) |
47 | 44, 46 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) |
48 | | mplind.sk |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (Base‘𝑅) |
49 | 43 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑌))) |
50 | 48, 49 | syl5eq 2668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑌))) |
51 | 47, 50 | eleqtrrd 2704 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(1r‘(Scalar‘𝑌)) ∈ 𝐾) |
52 | | mplind.s |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻) |
53 | 52 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻) |
54 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 =
(1r‘(Scalar‘𝑌)) → (𝐶‘𝑥) = (𝐶‘(1r‘(Scalar‘𝑌)))) |
55 | 54 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑥 =
(1r‘(Scalar‘𝑌)) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘(1r‘(Scalar‘𝑌))) ∈ 𝐻)) |
56 | 55 | rspcva 3307 |
. . . . . . . . . . . 12
⊢
(((1r‘(Scalar‘𝑌)) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻) → (𝐶‘(1r‘(Scalar‘𝑌))) ∈ 𝐻) |
57 | 51, 53, 56 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘(1r‘(Scalar‘𝑌))) ∈ 𝐻) |
58 | 42, 57 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑌) ∈ 𝐻) |
59 | | assaring 19320 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ Ring) |
60 | 34, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Ring) |
61 | 8, 40 | ringidcl 18568 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Ring →
(1r‘𝑌)
∈ 𝐵) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑌) ∈ 𝐵) |
63 | 58, 62 | elind 3798 |
. . . . . . . . 9
⊢ (𝜑 → (1r‘𝑌) ∈ (𝐻 ∩ 𝐵)) |
64 | | ne0i 3921 |
. . . . . . . . 9
⊢
((1r‘𝑌) ∈ (𝐻 ∩ 𝐵) → (𝐻 ∩ 𝐵) ≠ ∅) |
65 | 63, 64 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 ∩ 𝐵) ≠ ∅) |
66 | 1 | sseli 3599 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐻 ∩ 𝐵) → 𝑧 ∈ 𝐻) |
67 | 1 | sseli 3599 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝐻 ∩ 𝐵) → 𝑤 ∈ 𝐻) |
68 | 66, 67 | anim12i 590 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) |
69 | | mplind.p |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻) |
70 | 69 | caovclg 6826 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → (𝑧 + 𝑤) ∈ 𝐻) |
71 | 68, 70 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐻) |
72 | | assalmod 19319 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ LMod) |
73 | 34, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ LMod) |
74 | | lmodgrp 18870 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ LMod → 𝑌 ∈ Grp) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ Grp) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Grp) |
77 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (𝐻 ∩ 𝐵)) |
78 | 6, 77 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐵) |
79 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵)) |
80 | 6, 79 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵) |
81 | | mplind.sp |
. . . . . . . . . . . . . . 15
⊢ + =
(+g‘𝑌) |
82 | 8, 81 | grpcl 17430 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵) |
83 | 76, 78, 80, 82 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐵) |
84 | 71, 83 | elind 3798 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵)) |
85 | 84 | anassrs 680 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵)) |
86 | 85 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵)) |
87 | | mplind.st |
. . . . . . . . . . . . 13
⊢ · =
(.r‘𝑌) |
88 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(invg‘𝑌) = (invg‘𝑌) |
89 | 60 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Ring) |
90 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ (𝐻 ∩ 𝐵)) |
91 | 6, 90 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐵) |
92 | 8, 87, 40, 88, 89, 91 | ringnegl 18594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((invg‘𝑌)‘(1r‘𝑌)) · 𝑧) = ((invg‘𝑌)‘𝑧)) |
93 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝜑) |
94 | | rhmghm 18725 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌)) |
95 | 38, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌)) |
96 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(invg‘(Scalar‘𝑌)) =
(invg‘(Scalar‘𝑌)) |
97 | 45, 96, 88 | ghminv 17667 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌) ∧
(1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) = ((invg‘𝑌)‘(𝐶‘(1r‘(Scalar‘𝑌))))) |
98 | 95, 47, 97 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) = ((invg‘𝑌)‘(𝐶‘(1r‘(Scalar‘𝑌))))) |
99 | 42 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
((invg‘𝑌)‘(𝐶‘(1r‘(Scalar‘𝑌)))) =
((invg‘𝑌)‘(1r‘𝑌))) |
100 | 98, 99 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) = ((invg‘𝑌)‘(1r‘𝑌))) |
101 | | ringgrp 18552 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Scalar‘𝑌)
∈ Ring → (Scalar‘𝑌) ∈ Grp) |
102 | 44, 101 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Scalar‘𝑌) ∈ Grp) |
103 | 45, 96 | grpinvcl 17467 |
. . . . . . . . . . . . . . . . . 18
⊢
(((Scalar‘𝑌)
∈ Grp ∧ (1r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) →
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) ∈
(Base‘(Scalar‘𝑌))) |
104 | 102, 47, 103 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) ∈
(Base‘(Scalar‘𝑌))) |
105 | 104, 50 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) ∈ 𝐾) |
106 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) → (𝐶‘𝑥) = (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))))) |
107 | 106 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) ∈ 𝐻)) |
108 | 107 | rspcva 3307 |
. . . . . . . . . . . . . . . 16
⊢
((((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌))) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻) → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) ∈ 𝐻) |
109 | 105, 53, 108 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘((invg‘(Scalar‘𝑌))‘(1r‘(Scalar‘𝑌)))) ∈ 𝐻) |
110 | 100, 109 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((invg‘𝑌)‘(1r‘𝑌)) ∈ 𝐻) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘(1r‘𝑌)) ∈ 𝐻) |
112 | 1, 90 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐻) |
113 | | mplind.t |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻) |
114 | 113 | caovclg 6826 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧
(((invg‘𝑌)‘(1r‘𝑌)) ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (((invg‘𝑌)‘(1r‘𝑌)) · 𝑧) ∈ 𝐻) |
115 | 93, 111, 112, 114 | syl12anc 1324 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((invg‘𝑌)‘(1r‘𝑌)) · 𝑧) ∈ 𝐻) |
116 | 92, 115 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘𝑧) ∈ 𝐻) |
117 | 75 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Grp) |
118 | 8, 88 | grpinvcl 17467 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵) → ((invg‘𝑌)‘𝑧) ∈ 𝐵) |
119 | 117, 91, 118 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘𝑧) ∈ 𝐵) |
120 | 116, 119 | elind 3798 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)) |
121 | 86, 120 | jca 554 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))) |
122 | 121 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))) |
123 | 8, 81, 88 | issubg2 17609 |
. . . . . . . . 9
⊢ (𝑌 ∈ Grp → ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐻 ∩ 𝐵) ≠ ∅ ∧ ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))))) |
124 | 75, 123 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐻 ∩ 𝐵) ≠ ∅ ∧ ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((invg‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))))) |
125 | 32, 65, 122, 124 | mpbir3and 1245 |
. . . . . . 7
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌)) |
126 | 1 | sseli 3599 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐻 ∩ 𝐵) → 𝑥 ∈ 𝐻) |
127 | 1 | sseli 3599 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐻 ∩ 𝐵) → 𝑦 ∈ 𝐻) |
128 | 126, 127 | anim12i 590 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵)) → (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) |
129 | 128, 113 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐻) |
130 | 60 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Ring) |
131 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ (𝐻 ∩ 𝐵)) |
132 | 6, 131 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ 𝐵) |
133 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ (𝐻 ∩ 𝐵)) |
134 | 6, 133 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ 𝐵) |
135 | 8, 87 | ringcl 18561 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
136 | 130, 132,
134, 135 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐵) |
137 | 129, 136 | elind 3798 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)) |
138 | 137 | ralrimivva 2971 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)) |
139 | 8, 40, 87 | issubrg2 18800 |
. . . . . . . 8
⊢ (𝑌 ∈ Ring → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ (1r‘𝑌) ∈ (𝐻 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)))) |
140 | 60, 139 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ (1r‘𝑌) ∈ (𝐻 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵)))) |
141 | 125, 63, 138, 140 | mpbir3and 1245 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌)) |
142 | 7, 2, 8 | mplval2 19431 |
. . . . . . . 8
⊢ 𝑌 = ((𝐼 mPwSer 𝑅) ↾s 𝐵) |
143 | 142 | subsubrg 18806 |
. . . . . . 7
⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ⊆ 𝐵))) |
144 | 143 | simprbda 653 |
. . . . . 6
⊢ ((𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌)) → (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
145 | 11, 141, 144 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
146 | | assalmod 19319 |
. . . . . . 7
⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ LMod) |
147 | 5, 146 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ LMod) |
148 | 2, 7, 8, 3, 10 | mpllss 19438 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) |
149 | 34 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ AssAlg) |
150 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (Base‘(Scalar‘𝑌))) |
151 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵)) |
152 | 6, 151 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵) |
153 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
154 | 35, 36, 45, 8, 87, 153 | asclmul1 19339 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ AssAlg ∧ 𝑧 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·𝑠
‘𝑌)𝑤)) |
155 | 149, 150,
152, 154 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·𝑠
‘𝑌)𝑤)) |
156 | 50 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝐾 = (Base‘(Scalar‘𝑌))) |
157 | 150, 156 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐾) |
158 | 53 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻) |
159 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝐶‘𝑥) = (𝐶‘𝑧)) |
160 | 159 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘𝑧) ∈ 𝐻)) |
161 | 160 | rspcva 3307 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻) → (𝐶‘𝑧) ∈ 𝐻) |
162 | 157, 158,
161 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝐶‘𝑧) ∈ 𝐻) |
163 | 1, 151 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐻) |
164 | 162, 163 | jca 554 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) |
165 | 113 | caovclg 6826 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻) |
166 | 164, 165 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻) |
167 | 155, 166 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ 𝐻) |
168 | 73 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ LMod) |
169 | 8, 36, 153, 45 | lmodvscl 18880 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ LMod ∧ 𝑧 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ 𝐵) |
170 | 168, 150,
152, 169 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ 𝐵) |
171 | 167, 170 | elind 3798 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)) |
172 | 171 | ralrimivva 2971 |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)) |
173 | | eqid 2622 |
. . . . . . . . 9
⊢
(LSubSp‘𝑌) =
(LSubSp‘𝑌) |
174 | 36, 45, 8, 153, 173 | islss4 18962 |
. . . . . . . 8
⊢ (𝑌 ∈ LMod → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)))) |
175 | 73, 174 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·𝑠
‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵)))) |
176 | 125, 172,
175 | mpbir2and 957 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌)) |
177 | | eqid 2622 |
. . . . . . . 8
⊢
(LSubSp‘(𝐼
mPwSer 𝑅)) =
(LSubSp‘(𝐼 mPwSer
𝑅)) |
178 | 142, 177,
173 | lsslss 18961 |
. . . . . . 7
⊢ (((𝐼 mPwSer 𝑅) ∈ LMod ∧ 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ⊆ 𝐵))) |
179 | 178 | simprbda 653 |
. . . . . 6
⊢ ((((𝐼 mPwSer 𝑅) ∈ LMod ∧ 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) ∧ (𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌)) → (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) |
180 | 147, 148,
176, 179 | syl21anc 1325 |
. . . . 5
⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) |
181 | 27, 12, 177 | aspid 19330 |
. . . . 5
⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵)) |
182 | 5, 145, 180, 181 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵)) |
183 | 29, 31, 182 | 3sstr3d 3647 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ (𝐻 ∩ 𝐵)) |
184 | | mplind.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
185 | 183, 184 | sseldd 3604 |
. 2
⊢ (𝜑 → 𝑋 ∈ (𝐻 ∩ 𝐵)) |
186 | 1, 185 | sseldi 3601 |
1
⊢ (𝜑 → 𝑋 ∈ 𝐻) |