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 
|- K = ( Base ` R )
mplind.sv 
|- V = ( I mVar R )
mplind.sy 
|- Y = ( I mPoly R )
mplind.sp 
|- .+ = ( +g ` Y )
mplind.st 
|- .x. = ( .r ` Y )
mplind.sc 
|- C = ( algSc ` Y )
mplind.sb 
|- B = ( Base ` Y )
mplind.p 
|- ( ( ph /\ ( x e. H /\ y e. H ) ) -> ( x .+ y ) e. H )
mplind.t 
|- ( ( ph /\ ( x e. H /\ y e. H ) ) -> ( x .x. y ) e. H )
mplind.s 
|- ( ( ph /\ x e. K ) -> ( C ` x ) e. H )
mplind.v 
|- ( ( ph /\ x e. I ) -> ( V ` x ) e. H )
mplind.x 
|- ( ph -> X e. B )
mplind.i 
|- ( ph -> I e. W )
mplind.r 
|- ( ph -> R e. CRing )
Assertion mplind 
|- ( ph -> X e. H )

Proof

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