This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 89 88 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 12 adantr 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
114 7 adantr 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> G e. ( SubDRing ` L ) )
115 simpr 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> a e. ( G ^m B ) )
116 113 114 115 elmaprd 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> a : B --> G )
117 116 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 )
118 117 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 )
119 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 )
120 118 119 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 )
121 120 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 )
122 111 112 121 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 ) )
123 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 )
124 121 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 ) ) ) )
125 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 ) )
126 116 ffnd 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> a Fn B )
127 126 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 )
128 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 ) ) )
129 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 )
130 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 )
131 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 ) ) ) )
132 131 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 ) ) )
133 130 132 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 ) ) ) )
134 127 128 129 133 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 ) )
135 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 ) )
136 134 135 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 ) )
137 136 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 ) ) )
138 122 123 124 125 137 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 ) )
139 eqid 
 |-  ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) ) = ( g e. H |-> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) )
140 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> g = f )
141 suppssdm 
 |-  ( a supp ( 0g ` L ) ) C_ dom a
142 116 fdmd 
 |-  ( ( ph /\ a e. ( G ^m B ) ) -> dom a = B )
143 142 adantr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> dom a = B )
144 141 143 sseqtrid 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( a supp ( 0g ` L ) ) C_ B )
145 144 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> f e. B )
146 145 adantr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> f e. B )
147 140 146 eqeltrd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> g e. B )
148 147 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 ) )
149 fveq2 
 |-  ( g = f -> ( a ` g ) = ( a ` f ) )
150 149 adantl 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) /\ g = f ) -> ( a ` g ) = ( a ` f ) )
151 148 150 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 ) )
152 80 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> B C_ H )
153 144 152 sstrd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( a supp ( 0g ` L ) ) C_ H )
154 153 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> f e. H )
155 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( a supp ( 0g ` L ) ) ) -> ( a ` f ) e. _V )
156 139 151 154 155 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 ) )
157 156 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 ) )
158 157 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 ) ) )
159 fveq2 
 |-  ( f = v -> ( a ` f ) = ( a ` v ) )
160 id 
 |-  ( f = v -> f = v )
161 159 160 oveq12d 
 |-  ( f = v -> ( ( a ` f ) ( .r ` L ) f ) = ( ( a ` v ) ( .r ` L ) v ) )
162 161 cbvmptv 
 |-  ( f e. ( a supp ( 0g ` L ) ) |-> ( ( a ` f ) ( .r ` L ) f ) ) = ( v e. ( a supp ( 0g ` L ) ) |-> ( ( a ` v ) ( .r ` L ) v ) )
163 158 162 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 ) ) )
164 163 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 ) ) ) )
165 36 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> L e. CMnd )
166 8 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> H e. ( SubDRing ` L ) )
167 eleq1w 
 |-  ( g = f -> ( g e. B <-> f e. B ) )
168 167 149 ifbieq1d 
 |-  ( g = f -> if ( g e. B , ( a ` g ) , ( 0g ` L ) ) = if ( f e. B , ( a ` f ) , ( 0g ` L ) ) )
169 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 ) ) ) )
170 169 eldifad 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> f e. H )
171 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( a ` f ) e. _V )
172 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> ( 0g ` L ) e. _V )
173 171 172 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 )
174 139 168 170 173 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 ) ) )
175 174 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 ) )
176 126 ad3antrrr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> a Fn B )
177 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 ) ) )
178 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 )
179 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) /\ f e. B ) -> f e. B )
180 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 ) ) ) )
181 180 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 ) ) )
182 179 181 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 ) ) ) )
183 176 177 178 182 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 ) )
184 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 ) )
185 183 184 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 ) )
186 185 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 ) )
187 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> L e. Ring )
188 166 22 70 3syl 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> H C_ ( Base ` L ) )
189 188 ssdifssd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( H \ ( a supp ( 0g ` L ) ) ) C_ ( Base ` L ) )
190 189 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. ( H \ ( a supp ( 0g ` L ) ) ) ) -> f e. ( Base ` L ) )
191 16 17 18 187 190 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 ) )
192 175 186 191 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 ) )
193 simpr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> a finSupp ( 0g ` L ) )
194 193 fsuppimpd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( a supp ( 0g ` L ) ) e. Fin )
195 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. H ) -> L e. Ring )
196 26 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ g e. B ) -> G C_ ( Base ` L ) )
197 116 ad2antrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) -> a : B --> G )
198 197 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ g e. B ) -> ( a ` g ) e. G )
199 196 198 sseldd 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ g e. B ) -> ( a ` g ) e. ( Base ` L ) )
200 26 41 sseldd 
 |-  ( ph -> ( 0g ` L ) e. ( Base ` L ) )
201 200 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ g e. H ) /\ -. g e. B ) -> ( 0g ` L ) e. ( Base ` L ) )
202 199 201 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 ) )
203 202 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 ) )
204 203 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 ) )
205 188 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ f e. H ) -> f e. ( Base ` L ) )
206 16 17 195 204 205 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 ) )
207 16 18 165 166 192 194 206 153 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 ) ) ) )
208 113 adantr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
209 126 ad2antrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> a Fn B )
210 208 adantr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
211 fvexd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> ( 0g ` L ) e. _V )
212 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 ) ) ) )
213 209 210 211 212 fvdifsupp 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> ( a ` v ) = ( 0g ` L ) )
214 213 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 ) )
215 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> L e. Ring )
216 81 ad2antrr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> B C_ ( Base ` L ) )
217 216 ssdifssd 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> ( B \ ( a supp ( 0g ` L ) ) ) C_ ( Base ` L ) )
218 217 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. ( B \ ( a supp ( 0g ` L ) ) ) ) -> v e. ( Base ` L ) )
219 16 17 18 215 218 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 ) )
220 214 219 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 ) )
221 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> L e. Ring )
222 26 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> G C_ ( Base ` L ) )
223 116 adantr 
 |-  ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) -> a : B --> G )
224 223 ffvelcdmda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> ( a ` v ) e. G )
225 222 224 sseldd 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> ( a ` v ) e. ( Base ` L ) )
226 216 sselda 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> v e. ( Base ` L ) )
227 16 17 221 225 226 ringcld 
 |-  ( ( ( ( ph /\ a e. ( G ^m B ) ) /\ a finSupp ( 0g ` L ) ) /\ v e. B ) -> ( ( a ` v ) ( .r ` L ) v ) e. ( Base ` L ) )
228 16 18 165 208 220 194 227 144 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 ) ) ) )
229 164 207 228 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 ) ) ) )
230 229 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 ) ) ) ) )
231 230 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 ) ) ) )
232 231 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 ) ) ) )
233 138 232 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 ) ) ) ) )
234 110 122 233 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 ) ) ) ) )
235 234 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 ) ) ) ) )
236 103 235 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 ) ) ) ) ) )
237 59 84 236 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 ) ) )
238 15 24 237 3bitrd 
 |-  ( ph -> ( x e. C <-> x e. ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) ) )
239 238 eqrdv 
 |-  ( ph -> C = ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) )