Metamath Proof Explorer

Theorem fldextrspunlsp

Description: Lemma for fldextrspunfld . The subring generated by the union of two field extensions G and H is the vector sub- G space generated by a basis B of H . Part of the proof of Proposition 5, Chapter 5, of BourbakiAlg2 p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses fldextrspunfld.k 
|- K = ( L |`s F )
fldextrspunfld.i 
|- I = ( L |`s G )
fldextrspunfld.j 
|- J = ( L |`s H )
fldextrspunfld.2 
|- ( ph -> L e. Field )
fldextrspunfld.3 
|- ( ph -> F e. ( SubDRing ` I ) )
fldextrspunfld.4 
|- ( ph -> F e. ( SubDRing ` J ) )
fldextrspunfld.5 
|- ( ph -> G e. ( SubDRing ` L ) )
fldextrspunfld.6 
|- ( ph -> H e. ( SubDRing ` L ) )
fldextrspunlsp.n 
|- N = ( RingSpan ` L )
fldextrspunlsp.c 
|- C = ( N ` ( G u. H ) )
fldextrspunlsp.e 
|- E = ( L |`s C )
fldextrspunlsp.1 
|- ( ph -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
fldextrspunlsp.2 
|- ( ph -> B e. Fin )
Assertion fldextrspunlsp 
|- ( ph -> C = ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) )

Proof

Step Hyp Ref Expression
1 fldextrspunfld.k 
 |-  K = ( L |`s F )
2 fldextrspunfld.i 
 |-  I = ( L |`s G )
3 fldextrspunfld.j 
 |-  J = ( L |`s H )
4 fldextrspunfld.2 
 |-  ( ph -> L e. Field )
5 fldextrspunfld.3 
 |-  ( ph -> F e. ( SubDRing ` I ) )
6 fldextrspunfld.4 
 |-  ( ph -> F e. ( SubDRing ` J ) )
7 fldextrspunfld.5 
 |-  ( ph -> G e. ( SubDRing ` L ) )
8 fldextrspunfld.6 
 |-  ( ph -> H e. ( SubDRing ` L ) )
9 fldextrspunlsp.n 
 |-  N = ( RingSpan ` L )
10 fldextrspunlsp.c 
 |-  C = ( N ` ( G u. H ) )
11 fldextrspunlsp.e 
 |-  E = ( L |`s C )
12 fldextrspunlsp.1 
 |-  ( ph -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
13 fldextrspunlsp.2 
 |-  ( ph -> B e. Fin )
14 10 a1i 
 |-  ( ph -> C = ( N ` ( G u. H ) ) )
15 14 eleq2d 
 |-  ( ph -> ( x e. C <-> x e. ( N ` ( G u. H ) ) ) )
16 eqid 
 |-  ( Base ` L ) = ( Base ` L )
17 eqid 
 |-  ( .r ` L ) = ( .r ` L )
18 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
19 4 fldcrngd 
 |-  ( ph -> L e. CRing )
20 sdrgsubrg 
 |-  ( G e. ( SubDRing ` L ) -> G e. ( SubRing ` L ) )
21 7 20 syl 
 |-  ( ph -> G e. ( SubRing ` L ) )
22 sdrgsubrg 
 |-  ( H e. ( SubDRing ` L ) -> H e. ( SubRing ` L ) )
23 8 22 syl 
 |-  ( ph -> H e. ( SubRing ` L ) )
24 16 17 18 9 19 21 23 elrgspnsubrun 
 |-  ( ph -> ( x e. ( N ` ( G u. H ) ) <-> E. p e. ( G ^m H ) ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) )
25 16 subrgss 
 |-  ( G e. ( SubRing ` L ) -> G C_ ( Base ` L ) )
26 21 25 syl 
 |-  ( ph -> G C_ ( Base ` L ) )
27 eqid 
 |-  ( L |`s G ) = ( L |`s G )
28 27 16 ressbas2 
 |-  ( G C_ ( Base ` L ) -> G = ( Base ` ( L |`s G ) ) )
29 26 28 syl 
 |-  ( ph -> G = ( Base ` ( L |`s G ) ) )
30 eqidd 
 |-  ( ph -> ( ( subringAlg ` L ) ` G ) = ( ( subringAlg ` L ) ` G ) )
31 30 26 srasca 
 |-  ( ph -> ( L |`s G ) = ( Scalar ` ( ( subringAlg ` L ) ` G ) ) )
32 31 fveq2d 
 |-  ( ph -> ( Base ` ( L |`s G ) ) = ( Base ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) )
33 29 32 eqtr2d 
 |-  ( ph -> ( Base ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) = G )
34 33 oveq1d 
 |-  ( ph -> ( ( Base ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) ^m B ) = ( G ^m B ) )
35 19 crngringd 
 |-  ( ph -> L e. Ring )
36 35 ringcmnd 
 |-  ( ph -> L e. CMnd )
37 36 cmnmndd 
 |-  ( ph -> L e. Mnd )
38 subrgsubg 
 |-  ( G e. ( SubRing ` L ) -> G e. ( SubGrp ` L ) )
39 21 38 syl 
 |-  ( ph -> G e. ( SubGrp ` L ) )
40 18 subg0cl 
 |-  ( G e. ( SubGrp ` L ) -> ( 0g ` L ) e. G )
41 39 40 syl 
 |-  ( ph -> ( 0g ` L ) e. G )
42 27 16 18 ress0g 
 |-  ( ( L e. Mnd /\ ( 0g ` L ) e. G /\ G C_ ( Base ` L ) ) -> ( 0g ` L ) = ( 0g ` ( L |`s G ) ) )
43 37 41 26 42 syl3anc 
 |-  ( ph -> ( 0g ` L ) = ( 0g ` ( L |`s G ) ) )
44 31 fveq2d 
 |-  ( ph -> ( 0g ` ( L |`s G ) ) = ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) )
45 43 44 eqtr2d 
 |-  ( ph -> ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) = ( 0g ` L ) )
46 45 breq2d 
 |-  ( ph -> ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) <-> a finSupp ( 0g ` L ) ) )
47 eqid 
 |-  ( ( subringAlg ` L ) ` G ) = ( ( subringAlg ` L ) ` G )
48 12 mptexd 
 |-  ( ph -> ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) e. _V )
49 47 sralmod 
 |-  ( G e. ( SubRing ` L ) -> ( ( subringAlg ` L ) ` G ) e. LMod )
50 21 49 syl 
 |-  ( ph -> ( ( subringAlg ` L ) ` G ) e. LMod )
51 47 48 4 50 26 gsumsra 
 |-  ( ph -> ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) = ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) )
52 30 26 sravsca 
 |-  ( ph -> ( .r ` L ) = ( .s ` ( ( subringAlg ` L ) ` G ) ) )
53 52 oveqd 
 |-  ( ph -> ( ( a ` v ) ( .r ` L ) v ) = ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) )
54 53 mpteq2dv 
 |-  ( ph -> ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) = ( v e. B |-> ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) ) )
55 54 oveq2d 
 |-  ( ph -> ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) = ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) ) ) )
56 51 55 eqtr2d 
 |-  ( ph -> ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) ) ) = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) )
57 56 eqeq2d 
 |-  ( ph -> ( x = ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) ) ) <-> x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) )
58 46 57 anbi12d 
 |-  ( ph -> ( ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) /\ x = ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) ) ) ) <-> ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) )
59 34 58 rexeqbidv 
 |-  ( ph -> ( E. a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) ^m B ) ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) /\ x = ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) ) ) ) <-> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) )
60 eqid 
 |-  ( LSpan ` ( ( subringAlg ` L ) ` G ) ) = ( LSpan ` ( ( subringAlg ` L ) ` G ) )
61 eqid 
 |-  ( Base ` ( ( subringAlg ` L ) ` G ) ) = ( Base ` ( ( subringAlg ` L ) ` G ) )
62 eqid 
 |-  ( Base ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) = ( Base ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) )
63 eqid 
 |-  ( Scalar ` ( ( subringAlg ` L ) ` G ) ) = ( Scalar ` ( ( subringAlg ` L ) ` G ) )
64 eqid 
 |-  ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) = ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) )
65 eqid 
 |-  ( .s ` ( ( subringAlg ` L ) ` G ) ) = ( .s ` ( ( subringAlg ` L ) ` G ) )
66 eqid 
 |-  ( Base ` ( ( subringAlg ` J ) ` F ) ) = ( Base ` ( ( subringAlg ` J ) ` F ) )
67 eqid 
 |-  ( LBasis ` ( ( subringAlg ` J ) ` F ) ) = ( LBasis ` ( ( subringAlg ` J ) ` F ) )
68 66 67 lbsss 
 |-  ( B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) -> B C_ ( Base ` ( ( subringAlg ` J ) ` F ) ) )
69 12 68 syl 
 |-  ( ph -> B C_ ( Base ` ( ( subringAlg ` J ) ` F ) ) )
70 16 subrgss 
 |-  ( H e. ( SubRing ` L ) -> H C_ ( Base ` L ) )
71 23 70 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
72 3 16 ressbas2 
 |-  ( H C_ ( Base ` L ) -> H = ( Base ` J ) )
73 71 72 syl 
 |-  ( ph -> H = ( Base ` J ) )
74 eqidd 
 |-  ( ph -> ( ( subringAlg ` J ) ` F ) = ( ( subringAlg ` J ) ` F ) )
75 eqid 
 |-  ( Base ` J ) = ( Base ` J )
76 75 sdrgss 
 |-  ( F e. ( SubDRing ` J ) -> F C_ ( Base ` J ) )
77 6 76 syl 
 |-  ( ph -> F C_ ( Base ` J ) )
78 74 77 srabase 
 |-  ( ph -> ( Base ` J ) = ( Base ` ( ( subringAlg ` J ) ` F ) ) )
79 73 78 eqtrd 
 |-  ( ph -> H = ( Base ` ( ( subringAlg ` J ) ` F ) ) )
80 69 79 sseqtrrd 
 |-  ( ph -> B C_ H )
81 80 71 sstrd 
 |-  ( ph -> B C_ ( Base ` L ) )
82 30 26 srabase 
 |-  ( ph -> ( Base ` L ) = ( Base ` ( ( subringAlg ` L ) ` G ) ) )
83 81 82 sseqtrd 
 |-  ( ph -> B C_ ( Base ` ( ( subringAlg ` L ) ` G ) ) )
84 60 61 62 63 64 65 50 83 ellspds 
 |-  ( ph -> ( x e. ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) <-> E. a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) ^m B ) ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` L ) ` G ) ) ) /\ x = ( ( ( subringAlg ` L ) ` G ) gsum ( v e. B |-> ( ( a ` v ) ( .s ` ( ( subringAlg ` L ) ` G ) ) v ) ) ) ) ) )
85 4 ad2antrr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> L e. Field )
86 5 ad2antrr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> F e. ( SubDRing ` I ) )
87 6 ad2antrr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> F e. ( SubDRing ` J ) )
88 7 ad2antrr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> G e. ( SubDRing ` L ) )
89 8 ad2antrr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> H e. ( SubDRing ` L ) )
90 12 ad2antrr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
91 13 ad2antrr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> B e. Fin )
92 simplr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> p e. ( G ^m H ) )
93 92 elmaprd 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> p : H --> G )
94 simprl 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> p finSupp ( 0g ` L ) )
95 simprr 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) )
96 fveq2 
 |-  ( f = h -> ( p ` f ) = ( p ` h ) )
97 id 
 |-  ( f = h -> f = h )
98 96 97 oveq12d 
 |-  ( f = h -> ( ( p ` f ) ( .r ` L ) f ) = ( ( p ` h ) ( .r ` L ) h ) )
99 98 cbvmptv 
 |-  ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) = ( h e. H |-> ( ( p ` h ) ( .r ` L ) h ) )
100 99 oveq2i 
 |-  ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( h e. H |-> ( ( p ` h ) ( .r ` L ) h ) ) )
101 95 100 eqtrdi 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> x = ( L gsum ( h e. H |-> ( ( p ` h ) ( .r ` L ) h ) ) ) )
102 1 2 3 85 86 87 88 89 9 10 11 90 91 93 94 101 fldextrspunlsplem 
 |-  ( ( ( ph /\ p e. ( G ^m H ) ) /\ ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) )
103 102 r19.29an 
 |-  ( ( ph /\ E. p e. ( G ^m H ) ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) ) -> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) )
104 breq1 
 |-  ( p = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) -> ( p finSupp ( 0g ` L ) <-> ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) finSupp ( 0g ` L ) ) )
105 fveq1 
 |-  ( p = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) -> ( p ` f ) = ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) )
106 105 oveq1d 
 |-  ( p = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) -> ( ( p ` f ) ( .r ` L ) f ) = ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) )
107 106 mpteq2dv 
 |-  ( p = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) -> ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) = ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) )
108 107 oveq2d 
 |-  ( p = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) -> ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) )
109 108 eqeq2d 
 |-  ( p = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) -> ( x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) <-> x = ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) ) )
110 104 109 anbi12d 
 |-  ( p = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) -> ( ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) <-> ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) ) ) )
111 7 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> G e. ( SubDRing ` L ) )
112 8 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> H e. ( SubDRing ` L ) )
113 simpr 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> a e. ( G ^m B ) )
114 113 elmaprd 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> a : B --> G )
115 114 ad2antrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. H ) -> a : B --> G )
116 115 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. H ) /\ g e. B ) -> ( a ` g ) e. G )
117 41 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. H ) /\ -. g e. B ) -> ( 0g ` L ) e. G )
118 116 117 ifclda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. H ) -> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) e. G )
119 118 fmpttd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) : H --> G )
120 111 112 119 elmapdd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) e. ( G ^m H ) )
121 fvexd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> ( 0g ` L ) e. _V )
122 119 ffund 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> Fun ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) )
123 simprl 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> a finSupp ( 0g ` L ) )
124 114 ffnd 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> a Fn B )
125 124 ad3antrrr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> a Fn B )
126 12 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
127 fvexd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> ( 0g ` L ) e. _V )
128 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> g e. B )
129 simplr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> g e. ( H \ ( a supp ( 0g ` L ) ) ) )
130 129 eldifbd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> -. g e. ( a supp ( 0g ` L ) ) )
131 128 130 eldifd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> g e. ( B \ ( a supp ( 0g ` L ) ) ) )
132 125 126 127 131 fvdifsupp 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ g e. B ) -> ( a ` g ) = ( 0g ` L ) )
133 eqidd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ -. g e. B ) -> ( 0g ` L ) = ( 0g ` L ) )
134 132 133 ifeqda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) /\ g e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) = ( 0g ` L ) )
135 134 112 suppss2 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) supp ( 0g ` L ) ) C_ ( a supp ( 0g ` L ) ) )
136 120 121 122 123 135 fsuppsssuppgd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) finSupp ( 0g ` L ) )
137 eqid 
 |-  ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) )
138 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> g = f )
139 suppssdm 
 |-  ( a supp ( 0g ` L ) ) C_ dom a
140 114 fdmd 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> dom a = B )
141 140 adantr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> dom a = B )
142 139 141 sseqtrid 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( a supp ( 0g ` L ) ) C_ B )
143 142 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> f e. B )
144 143 adantr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> f e. B )
145 138 144 eqeltrd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> g e. B )
146 145 iftrued 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) = ( a ` g ) )
147 fveq2 
 |-  ( g = f -> ( a ` g ) = ( a ` f ) )
148 147 adantl 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> ( a ` g ) = ( a ` f ) )
149 146 148 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) = ( a ` f ) )
150 80 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> B C_ H )
151 142 150 sstrd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( a supp ( 0g ` L ) ) C_ H )
152 151 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> f e. H )
153 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> ( a ` f ) e. _V )
154 137 149 152 153 fvmptd2 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) = ( a ` f ) )
155 154 oveq1d 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) = ( ( a ` f ) ( .r ` L ) f ) )
156 155 mpteq2dva 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( f e. ( a supp ( 0g ` L ) ) |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) = ( f e. ( a supp ( 0g ` L ) ) |-> ( ( a ` f ) ( .r ` L ) f ) ) )
157 fveq2 
 |-  ( f = v -> ( a ` f ) = ( a ` v ) )
158 id 
 |-  ( f = v -> f = v )
159 157 158 oveq12d 
 |-  ( f = v -> ( ( a ` f ) ( .r ` L ) f ) = ( ( a ` v ) ( .r ` L ) v ) )
160 159 cbvmptv 
 |-  ( f e. ( a supp ( 0g ` L ) ) |-> ( ( a ` f ) ( .r ` L ) f ) ) = ( v e. ( a supp ( 0g ` L ) ) |-> ( ( a ` v ) ( .r ` L ) v ) )
161 156 160 eqtrdi 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( f e. ( a supp ( 0g ` L ) ) |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) = ( v e. ( a supp ( 0g ` L ) ) |-> ( ( a ` v ) ( .r ` L ) v ) ) )
162 161 oveq2d 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( L gsum ( f e. ( a supp ( 0g ` L ) ) |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( v e. ( a supp ( 0g ` L ) ) |-> ( ( a ` v ) ( .r ` L ) v ) ) ) )
163 36 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> L e. CMnd )
164 8 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> H e. ( SubDRing ` L ) )
165 eleq1w 
 |-  ( g = f -> ( g e. B <-> f e. B ) )
166 165 147 ifbieq1d 
 |-  ( g = f -> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) = if ( f e. B , ( a ` f ) , ( 0g ` L ) ) )
167 simpr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> f e. ( H \ ( a supp ( 0g ` L ) ) ) )
168 167 eldifad 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> f e. H )
169 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( a ` f ) e. _V )
170 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( 0g ` L ) e. _V )
171 169 170 ifcld 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> if ( f e. B , ( a ` f ) , ( 0g ` L ) ) e. _V )
172 137 166 168 171 fvmptd3 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) = if ( f e. B , ( a ` f ) , ( 0g ` L ) ) )
173 172 oveq1d 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) = ( if ( f e. B , ( a ` f ) , ( 0g ` L ) ) ( .r ` L ) f ) )
174 124 ad3antrrr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> a Fn B )
175 12 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
176 fvexd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> ( 0g ` L ) e. _V )
177 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> f e. B )
178 simplr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> f e. ( H \ ( a supp ( 0g ` L ) ) ) )
179 178 eldifbd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> -. f e. ( a supp ( 0g ` L ) ) )
180 177 179 eldifd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> f e. ( B \ ( a supp ( 0g ` L ) ) ) )
181 174 175 176 180 fvdifsupp 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> ( a ` f ) = ( 0g ` L ) )
182 eqidd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ -. f e. B ) -> ( 0g ` L ) = ( 0g ` L ) )
183 181 182 ifeqda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> if ( f e. B , ( a ` f ) , ( 0g ` L ) ) = ( 0g ` L ) )
184 183 oveq1d 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( if ( f e. B , ( a ` f ) , ( 0g ` L ) ) ( .r ` L ) f ) = ( ( 0g ` L ) ( .r ` L ) f ) )
185 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> L e. Ring )
186 164 22 70 3syl 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> H C_ ( Base ` L ) )
187 186 ssdifssd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( H \ ( a supp ( 0g ` L ) ) ) C_ ( Base ` L ) )
188 187 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> f e. ( Base ` L ) )
189 16 17 18 185 188 ringlzd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( ( 0g ` L ) ( .r ` L ) f ) = ( 0g ` L ) )
190 173 184 189 3eqtrd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) = ( 0g ` L ) )
191 simpr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> a finSupp ( 0g ` L ) )
192 191 fsuppimpd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( a supp ( 0g ` L ) ) e. Fin )
193 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. H ) -> L e. Ring )
194 26 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ g e. B ) -> G C_ ( Base ` L ) )
195 114 ad2antrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) -> a : B --> G )
196 195 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ g e. B ) -> ( a ` g ) e. G )
197 194 196 sseldd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ g e. B ) -> ( a ` g ) e. ( Base ` L ) )
198 26 41 sseldd 
 |-  ( ph -> ( 0g ` L ) e. ( Base ` L ) )
199 198 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ -. g e. B ) -> ( 0g ` L ) e. ( Base ` L ) )
200 197 199 ifclda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) -> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) e. ( Base ` L ) )
201 200 fmpttd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) : H --> ( Base ` L ) )
202 201 ffvelcdmda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. H ) -> ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) e. ( Base ` L ) )
203 186 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. H ) -> f e. ( Base ` L ) )
204 16 17 193 202 203 ringcld 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. H ) -> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) e. ( Base ` L ) )
205 16 18 163 164 190 192 204 151 gsummptres2 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( f e. ( a supp ( 0g ` L ) ) |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) )
206 12 adantr 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
207 206 adantr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
208 124 ad2antrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> a Fn B )
209 207 adantr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
210 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> ( 0g ` L ) e. _V )
211 simpr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> v e. ( B \ ( a supp ( 0g ` L ) ) ) )
212 208 209 210 211 fvdifsupp 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> ( a ` v ) = ( 0g ` L ) )
213 212 oveq1d 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> ( ( a ` v ) ( .r ` L ) v ) = ( ( 0g ` L ) ( .r ` L ) v ) )
214 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> L e. Ring )
215 81 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> B C_ ( Base ` L ) )
216 215 ssdifssd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( B \ ( a supp ( 0g ` L ) ) ) C_ ( Base ` L ) )
217 216 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> v e. ( Base ` L ) )
218 16 17 18 214 217 ringlzd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> ( ( 0g ` L ) ( .r ` L ) v ) = ( 0g ` L ) )
219 213 218 eqtrd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> ( ( a ` v ) ( .r ` L ) v ) = ( 0g ` L ) )
220 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> L e. Ring )
221 26 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> G C_ ( Base ` L ) )
222 114 adantr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> a : B --> G )
223 222 ffvelcdmda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> ( a ` v ) e. G )
224 221 223 sseldd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> ( a ` v ) e. ( Base ` L ) )
225 215 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> v e. ( Base ` L ) )
226 16 17 220 224 225 ringcld 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> ( ( a ` v ) ( .r ` L ) v ) e. ( Base ` L ) )
227 16 18 163 207 219 192 226 142 gsummptres2 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) = ( L gsum ( v e. ( a supp ( 0g ` L ) ) |-> ( ( a ` v ) ( .r ` L ) v ) ) ) )
228 162 205 227 3eqtr4d 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) )
229 228 eqeq2d 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( x = ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) <-> x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) )
230 229 biimpar 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) -> x = ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) )
231 230 anasss 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> x = ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) )
232 136 231 jca 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) ` f ) ( .r ` L ) f ) ) ) ) )
233 110 120 232 rspcedvdw 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> E. p e. ( G ^m H ) ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) )
234 233 r19.29an 
 |-  ( ( ph /\ E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) -> E. p e. ( G ^m H ) ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) )
235 103 234 impbida 
 |-  ( ph -> ( E. p e. ( G ^m H ) ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) <-> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ x = ( L gsum ( v e. B |-> ( ( a ` v ) ( .r ` L ) v ) ) ) ) ) )
236 59 84 235 3bitr4rd 
 |-  ( ph -> ( E. p e. ( G ^m H ) ( p finSupp ( 0g ` L ) /\ x = ( L gsum ( f e. H |-> ( ( p ` f ) ( .r ` L ) f ) ) ) ) <-> x e. ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) ) )
237 15 24 236 3bitrd 
 |-  ( ph -> ( x e. C <-> x e. ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) ) )
238 237 eqrdv 
 |-  ( ph -> C = ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) )