Metamath Proof Explorer

Theorem mplind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. The commutativity condition is stronger than strictly needed. (Contributed by Stefan O'Rear, 11-Mar-2015)

Ref Expression
Hypotheses mplind.sk ⊢ 𝐾 = ( Base ‘ 𝑅 )
mplind.sv ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mplind.sy ⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
mplind.sp ⊢ + = ( +g ‘ 𝑌 )
mplind.st ⊢ · = ( .r ‘ 𝑌 )
mplind.sc ⊢ 𝐶 = ( algSc ‘ 𝑌 )
mplind.sb ⊢ 𝐵 = ( Base ‘ 𝑌 )
mplind.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐻 )
mplind.t ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐻 )
mplind.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( 𝐶 ‘ 𝑥 ) ∈ 𝐻 )
mplind.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑥 ) ∈ 𝐻 )
mplind.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mplind.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplind.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion mplind ( 𝜑 → 𝑋 ∈ 𝐻 )

Proof

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