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

Metamath Proof Explorer

Theorem fldextrspunlsplem

Description: Lemma for fldextrspunlsp : First direction. 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 )
fldextrspunlsplem.2 
|- ( ph -> P : H --> G )
fldextrspunlsplem.3 
|- ( ph -> P finSupp ( 0g ` L ) )
fldextrspunlsplem.4 
|- ( ph -> X = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) ) )
Assertion fldextrspunlsplem 
|- ( ph -> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) 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 fldextrspunlsplem.2 
 |-  ( ph -> P : H --> G )
15 fldextrspunlsplem.3 
 |-  ( ph -> P finSupp ( 0g ` L ) )
16 fldextrspunlsplem.4 
 |-  ( ph -> X = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) ) )
17 7 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> G e. ( SubDRing ` L ) )
18 12 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
19 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
20 4 flddrngd 
 |-  ( ph -> L e. DivRing )
21 20 drngringd 
 |-  ( ph -> L e. Ring )
22 21 ringcmnd 
 |-  ( ph -> L e. CMnd )
23 22 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> L e. CMnd )
24 8 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> H e. ( SubDRing ` L ) )
25 sdrgsubrg 
 |-  ( G e. ( SubDRing ` L ) -> G e. ( SubRing ` L ) )
26 7 25 syl 
 |-  ( ph -> G e. ( SubRing ` L ) )
27 subrgsubg 
 |-  ( G e. ( SubRing ` L ) -> G e. ( SubGrp ` L ) )
28 subgsubm 
 |-  ( G e. ( SubGrp ` L ) -> G e. ( SubMnd ` L ) )
29 26 27 28 3syl 
 |-  ( ph -> G e. ( SubMnd ` L ) )
30 29 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> G e. ( SubMnd ` L ) )
31 eqid 
 |-  ( .r ` L ) = ( .r ` L )
32 26 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> G e. ( SubRing ` L ) )
33 14 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> P : H --> G )
34 simpr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> f e. H )
35 33 34 ffvelcdmd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> ( P ` f ) e. G )
36 eqid 
 |-  ( Base ` I ) = ( Base ` I )
37 36 sdrgss 
 |-  ( F e. ( SubDRing ` I ) -> F C_ ( Base ` I ) )
38 5 37 syl 
 |-  ( ph -> F C_ ( Base ` I ) )
39 eqid 
 |-  ( Base ` L ) = ( Base ` L )
40 39 sdrgss 
 |-  ( G e. ( SubDRing ` L ) -> G C_ ( Base ` L ) )
41 7 40 syl 
 |-  ( ph -> G C_ ( Base ` L ) )
42 2 39 ressbas2 
 |-  ( G C_ ( Base ` L ) -> G = ( Base ` I ) )
43 41 42 syl 
 |-  ( ph -> G = ( Base ` I ) )
44 38 43 sseqtrrd 
 |-  ( ph -> F C_ G )
45 44 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> F C_ G )
46 12 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
47 5 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> F e. ( SubDRing ` I ) )
48 8 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> H e. ( SubDRing ` L ) )
49 ovexd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> ( F ^m B ) e. _V )
50 simpllr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> u e. ( ( F ^m B ) ^m H ) )
51 48 49 50 elmaprd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> u : H --> ( F ^m B ) )
52 51 34 ffvelcdmd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> ( u ` f ) e. ( F ^m B ) )
53 46 47 52 elmaprd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> ( u ` f ) : B --> F )
54 simplr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> c e. B )
55 53 54 ffvelcdmd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> ( ( u ` f ) ` c ) e. F )
56 45 55 sseldd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> ( ( u ` f ) ` c ) e. G )
57 31 32 35 56 subrgmcld 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) /\ f e. H ) -> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) e. G )
58 57 fmpttd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ c e. B ) -> ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) : H --> G )
59 58 adantlr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) : H --> G )
60 fveq2 
 |-  ( f = h -> ( P ` f ) = ( P ` h ) )
61 fveq2 
 |-  ( f = h -> ( u ` f ) = ( u ` h ) )
62 61 fveq1d 
 |-  ( f = h -> ( ( u ` f ) ` c ) = ( ( u ` h ) ` c ) )
63 60 62 oveq12d 
 |-  ( f = h -> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) = ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) )
64 63 cbvmptv 
 |-  ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) = ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) )
65 fvexd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( 0g ` L ) e. _V )
66 ssidd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> H C_ H )
67 eqid 
 |-  ( Base ` J ) = ( Base ` J )
68 67 sdrgss 
 |-  ( F e. ( SubDRing ` J ) -> F C_ ( Base ` J ) )
69 6 68 syl 
 |-  ( ph -> F C_ ( Base ` J ) )
70 39 sdrgss 
 |-  ( H e. ( SubDRing ` L ) -> H C_ ( Base ` L ) )
71 8 70 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
72 3 39 ressbas2 
 |-  ( H C_ ( Base ` L ) -> H = ( Base ` J ) )
73 71 72 syl 
 |-  ( ph -> H = ( Base ` J ) )
74 69 73 sseqtrrd 
 |-  ( ph -> F C_ H )
75 74 71 sstrd 
 |-  ( ph -> F C_ ( Base ` L ) )
76 75 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> F C_ ( Base ` L ) )
77 12 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
78 6 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> F e. ( SubDRing ` J ) )
79 ovexd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( F ^m B ) e. _V )
80 simpllr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> u e. ( ( F ^m B ) ^m H ) )
81 24 79 80 elmaprd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> u : H --> ( F ^m B ) )
82 81 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( u ` h ) e. ( F ^m B ) )
83 77 78 82 elmaprd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( u ` h ) : B --> F )
84 simplr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> c e. B )
85 83 84 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( ( u ` h ) ` c ) e. F )
86 76 85 sseldd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( ( u ` h ) ` c ) e. ( Base ` L ) )
87 14 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> P : H --> G )
88 15 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> P finSupp ( 0g ` L ) )
89 21 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ y e. ( Base ` L ) ) -> L e. Ring )
90 simpr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ y e. ( Base ` L ) ) -> y e. ( Base ` L ) )
91 39 31 19 89 90 ringlzd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ y e. ( Base ` L ) ) -> ( ( 0g ` L ) ( .r ` L ) y ) = ( 0g ` L ) )
92 65 65 24 66 86 87 88 91 fisuppov1 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) finSupp ( 0g ` L ) )
93 64 92 eqbrtrid 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) finSupp ( 0g ` L ) )
94 19 23 24 30 59 93 gsumsubmcl 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) e. G )
95 94 fmpttd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) : B --> G )
96 17 18 95 elmapdd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) e. ( G ^m B ) )
97 breq1 
 |-  ( a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) -> ( a finSupp ( 0g ` L ) <-> ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) finSupp ( 0g ` L ) ) )
98 97 adantl 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) -> ( a finSupp ( 0g ` L ) <-> ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) finSupp ( 0g ` L ) ) )
99 simplr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) /\ b e. B ) -> a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) )
100 99 fveq1d 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) /\ b e. B ) -> ( a ` b ) = ( ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ` b ) )
101 eqid 
 |-  ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) )
102 fveq2 
 |-  ( c = b -> ( ( u ` f ) ` c ) = ( ( u ` f ) ` b ) )
103 102 oveq2d 
 |-  ( c = b -> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) = ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) )
104 103 mpteq2dv 
 |-  ( c = b -> ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) = ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) )
105 104 oveq2d 
 |-  ( c = b -> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) )
106 simpr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ b e. B ) -> b e. B )
107 ovexd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ b e. B ) -> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) e. _V )
108 101 105 106 107 fvmptd3 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ b e. B ) -> ( ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ` b ) = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) )
109 108 adantlr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) /\ b e. B ) -> ( ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ` b ) = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) )
110 100 109 eqtrd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) /\ b e. B ) -> ( a ` b ) = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) )
111 110 oveq1d 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) /\ b e. B ) -> ( ( a ` b ) ( .r ` L ) b ) = ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) )
112 111 mpteq2dva 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) -> ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) = ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) )
113 112 oveq2d 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) -> ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) ) = ( L gsum ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) ) )
114 113 eqeq2d 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) -> ( X = ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) ) <-> X = ( L gsum ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) ) ) )
115 98 114 anbi12d 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) -> ( ( a finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) ) ) <-> ( ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) ) ) ) )
116 115 adantlr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ a = ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) ) -> ( ( a finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) ) ) <-> ( ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) ) ) ) )
117 13 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> B e. Fin )
118 ovexd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) e. _V )
119 fvexd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( 0g ` L ) e. _V )
120 101 117 118 119 fsuppmptdm 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) finSupp ( 0g ` L ) )
121 16 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> X = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) ) )
122 21 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> L e. Ring )
123 122 adantr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> L e. Ring )
124 12 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
125 41 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> G C_ ( Base ` L ) )
126 14 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> P : H --> G )
127 126 ffvelcdmda 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( P ` h ) e. G )
128 125 127 sseldd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( P ` h ) e. ( Base ` L ) )
129 123 adantr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> L e. Ring )
130 75 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> F C_ ( Base ` L ) )
131 12 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
132 6 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> F e. ( SubDRing ` J ) )
133 8 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> H e. ( SubDRing ` L ) )
134 ovexd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( F ^m B ) e. _V )
135 simp-4r 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> u e. ( ( F ^m B ) ^m H ) )
136 133 134 135 elmaprd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> u : H --> ( F ^m B ) )
137 simplr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> h e. H )
138 136 137 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( u ` h ) e. ( F ^m B ) )
139 131 132 138 elmaprd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( u ` h ) : B --> F )
140 simpr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> c e. B )
141 139 140 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( ( u ` h ) ` c ) e. F )
142 130 141 sseldd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( ( u ` h ) ` c ) e. ( Base ` L ) )
143 eqid 
 |-  ( Base ` ( ( subringAlg ` J ) ` F ) ) = ( Base ` ( ( subringAlg ` J ) ` F ) )
144 eqid 
 |-  ( LBasis ` ( ( subringAlg ` J ) ` F ) ) = ( LBasis ` ( ( subringAlg ` J ) ` F ) )
145 143 144 lbsss 
 |-  ( B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) -> B C_ ( Base ` ( ( subringAlg ` J ) ` F ) ) )
146 12 145 syl 
 |-  ( ph -> B C_ ( Base ` ( ( subringAlg ` J ) ` F ) ) )
147 eqidd 
 |-  ( ph -> ( ( subringAlg ` J ) ` F ) = ( ( subringAlg ` J ) ` F ) )
148 147 69 srabase 
 |-  ( ph -> ( Base ` J ) = ( Base ` ( ( subringAlg ` J ) ` F ) ) )
149 73 148 eqtr2d 
 |-  ( ph -> ( Base ` ( ( subringAlg ` J ) ` F ) ) = H )
150 146 149 sseqtrd 
 |-  ( ph -> B C_ H )
151 150 71 sstrd 
 |-  ( ph -> B C_ ( Base ` L ) )
152 151 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> B C_ ( Base ` L ) )
153 152 sselda 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> c e. ( Base ` L ) )
154 39 31 129 142 153 ringcld 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( ( ( u ` h ) ` c ) ( .r ` L ) c ) e. ( Base ` L ) )
155 fvexd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( 0g ` L ) e. _V )
156 ssidd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> B C_ B )
157 6 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> F e. ( SubDRing ` J ) )
158 8 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> H e. ( SubDRing ` L ) )
159 ovexd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( F ^m B ) e. _V )
160 simplr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> u e. ( ( F ^m B ) ^m H ) )
161 158 159 160 elmaprd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> u : H --> ( F ^m B ) )
162 161 ffvelcdmda 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( u ` h ) e. ( F ^m B ) )
163 124 157 162 elmaprd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( u ` h ) : B --> F )
164 61 breq1d 
 |-  ( f = h -> ( ( u ` f ) finSupp ( 0g ` L ) <-> ( u ` h ) finSupp ( 0g ` L ) ) )
165 id 
 |-  ( f = h -> f = h )
166 61 fveq1d 
 |-  ( f = h -> ( ( u ` f ) ` b ) = ( ( u ` h ) ` b ) )
167 166 oveq1d 
 |-  ( f = h -> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) = ( ( ( u ` h ) ` b ) ( .r ` L ) b ) )
168 167 mpteq2dv 
 |-  ( f = h -> ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) = ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) )
169 168 oveq2d 
 |-  ( f = h -> ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) = ( L gsum ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) ) )
170 165 169 eqeq12d 
 |-  ( f = h -> ( f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) <-> h = ( L gsum ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) ) ) )
171 164 170 anbi12d 
 |-  ( f = h -> ( ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) <-> ( ( u ` h ) finSupp ( 0g ` L ) /\ h = ( L gsum ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) ) ) ) )
172 simplr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) )
173 simpr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> h e. H )
174 171 172 173 rspcdva 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( ( u ` h ) finSupp ( 0g ` L ) /\ h = ( L gsum ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) ) ) )
175 174 simpld 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( u ` h ) finSupp ( 0g ` L ) )
176 123 adantr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ y e. ( Base ` L ) ) -> L e. Ring )
177 simpr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ y e. ( Base ` L ) ) -> y e. ( Base ` L ) )
178 39 31 19 176 177 ringlzd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ y e. ( Base ` L ) ) -> ( ( 0g ` L ) ( .r ` L ) y ) = ( 0g ` L ) )
179 155 155 124 156 153 163 175 178 fisuppov1 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( c e. B |-> ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) finSupp ( 0g ` L ) )
180 39 19 31 123 124 128 154 179 gsummulc2 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( L gsum ( c e. B |-> ( ( P ` h ) ( .r ` L ) ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) ) ) = ( ( P ` h ) ( .r ` L ) ( L gsum ( c e. B |-> ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) ) ) )
181 128 adantr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( P ` h ) e. ( Base ` L ) )
182 39 31 129 181 142 153 ringassd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) /\ c e. B ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( ( P ` h ) ( .r ` L ) ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) )
183 182 mpteq2dva 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( c e. B |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) = ( c e. B |-> ( ( P ` h ) ( .r ` L ) ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) ) )
184 183 oveq2d 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( L gsum ( c e. B |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) = ( L gsum ( c e. B |-> ( ( P ` h ) ( .r ` L ) ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) ) ) )
185 174 simprd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> h = ( L gsum ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) ) )
186 fveq2 
 |-  ( b = c -> ( ( u ` h ) ` b ) = ( ( u ` h ) ` c ) )
187 id 
 |-  ( b = c -> b = c )
188 186 187 oveq12d 
 |-  ( b = c -> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) = ( ( ( u ` h ) ` c ) ( .r ` L ) c ) )
189 188 cbvmptv 
 |-  ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) = ( c e. B |-> ( ( ( u ` h ) ` c ) ( .r ` L ) c ) )
190 189 oveq2i 
 |-  ( L gsum ( b e. B |-> ( ( ( u ` h ) ` b ) ( .r ` L ) b ) ) ) = ( L gsum ( c e. B |-> ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) )
191 185 190 eqtrdi 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> h = ( L gsum ( c e. B |-> ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) ) )
192 191 oveq2d 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( ( P ` h ) ( .r ` L ) h ) = ( ( P ` h ) ( .r ` L ) ( L gsum ( c e. B |-> ( ( ( u ` h ) ` c ) ( .r ` L ) c ) ) ) ) )
193 180 184 192 3eqtr4rd 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ h e. H ) -> ( ( P ` h ) ( .r ` L ) h ) = ( L gsum ( c e. B |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) )
194 193 mpteq2dva 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( h e. H |-> ( ( P ` h ) ( .r ` L ) h ) ) = ( h e. H |-> ( L gsum ( c e. B |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) ) )
195 194 oveq2d 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) h ) ) ) = ( L gsum ( h e. H |-> ( L gsum ( c e. B |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) ) ) )
196 60 165 oveq12d 
 |-  ( f = h -> ( ( P ` f ) ( .r ` L ) f ) = ( ( P ` h ) ( .r ` L ) h ) )
197 196 cbvmptv 
 |-  ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) = ( h e. H |-> ( ( P ` h ) ( .r ` L ) h ) )
198 197 oveq2i 
 |-  ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) h ) ) )
199 198 a1i 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) h ) ) ) )
200 22 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> L e. CMnd )
201 21 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> L e. Ring )
202 41 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> G C_ ( Base ` L ) )
203 87 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( P ` h ) e. G )
204 202 203 sseldd 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( P ` h ) e. ( Base ` L ) )
205 39 31 201 204 86 ringcld 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) e. ( Base ` L ) )
206 151 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> B C_ ( Base ` L ) )
207 206 sselda 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> c e. ( Base ` L ) )
208 207 adantr 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> c e. ( Base ` L ) )
209 39 31 201 205 208 ringcld 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) e. ( Base ` L ) )
210 209 anasss 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ ( c e. B /\ h e. H ) ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) e. ( Base ` L ) )
211 15 fsuppimpd 
 |-  ( ph -> ( P supp ( 0g ` L ) ) e. Fin )
212 211 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( P supp ( 0g ` L ) ) e. Fin )
213 suppssdm 
 |-  ( P supp ( 0g ` L ) ) C_ dom P
214 213 14 fssdm 
 |-  ( ph -> ( P supp ( 0g ` L ) ) C_ H )
215 214 sseld 
 |-  ( ph -> ( f e. ( P supp ( 0g ` L ) ) -> f e. H ) )
216 215 adantr 
 |-  ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) -> ( f e. ( P supp ( 0g ` L ) ) -> f e. H ) )
217 simpr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ ( u ` f ) finSupp ( 0g ` L ) ) -> ( u ` f ) finSupp ( 0g ` L ) )
218 217 fsuppimpd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ ( u ` f ) finSupp ( 0g ` L ) ) -> ( ( u ` f ) supp ( 0g ` L ) ) e. Fin )
219 218 ex 
 |-  ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) -> ( ( u ` f ) finSupp ( 0g ` L ) -> ( ( u ` f ) supp ( 0g ` L ) ) e. Fin ) )
220 219 adantrd 
 |-  ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) -> ( ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) -> ( ( u ` f ) supp ( 0g ` L ) ) e. Fin ) )
221 216 220 imim12d 
 |-  ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) -> ( ( f e. H -> ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( f e. ( P supp ( 0g ` L ) ) -> ( ( u ` f ) supp ( 0g ` L ) ) e. Fin ) ) )
222 221 ralimdv2 
 |-  ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) -> ( A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) -> A. f e. ( P supp ( 0g ` L ) ) ( ( u ` f ) supp ( 0g ` L ) ) e. Fin ) )
223 222 imp 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> A. f e. ( P supp ( 0g ` L ) ) ( ( u ` f ) supp ( 0g ` L ) ) e. Fin )
224 fveq2 
 |-  ( f = i -> ( u ` f ) = ( u ` i ) )
225 224 oveq1d 
 |-  ( f = i -> ( ( u ` f ) supp ( 0g ` L ) ) = ( ( u ` i ) supp ( 0g ` L ) ) )
226 225 eleq1d 
 |-  ( f = i -> ( ( ( u ` f ) supp ( 0g ` L ) ) e. Fin <-> ( ( u ` i ) supp ( 0g ` L ) ) e. Fin ) )
227 226 cbvralvw 
 |-  ( A. f e. ( P supp ( 0g ` L ) ) ( ( u ` f ) supp ( 0g ` L ) ) e. Fin <-> A. i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) e. Fin )
228 223 227 sylib 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> A. i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) e. Fin )
229 iunfi 
 |-  ( ( ( P supp ( 0g ` L ) ) e. Fin /\ A. i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) e. Fin ) -> U_ i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) e. Fin )
230 212 228 229 syl2anc 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> U_ i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) e. Fin )
231 xpfi 
 |-  ( ( U_ i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) e. Fin /\ ( P supp ( 0g ` L ) ) e. Fin ) -> ( U_ i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) X. ( P supp ( 0g ` L ) ) ) e. Fin )
232 230 212 231 syl2anc 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( U_ i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) X. ( P supp ( 0g ` L ) ) ) e. Fin )
233 snssi 
 |-  ( i e. ( P supp ( 0g ` L ) ) -> { i } C_ ( P supp ( 0g ` L ) ) )
234 233 adantl 
 |-  ( ( ph /\ i e. ( P supp ( 0g ` L ) ) ) -> { i } C_ ( P supp ( 0g ` L ) ) )
235 234 iunxpssiun1 
 |-  ( ph -> U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) C_ ( U_ i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) X. ( P supp ( 0g ` L ) ) ) )
236 235 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) C_ ( U_ i e. ( P supp ( 0g ` L ) ) ( ( u ` i ) supp ( 0g ` L ) ) X. ( P supp ( 0g ` L ) ) ) )
237 232 236 ssfid 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) e. Fin )
238 14 ffnd 
 |-  ( ph -> P Fn H )
239 238 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> P Fn H )
240 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> H e. ( SubDRing ` L ) )
241 fvexd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( 0g ` L ) e. _V )
242 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> h e. H )
243 simpr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> -. h e. ( P supp ( 0g ` L ) ) )
244 242 243 eldifd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> h e. ( H \ ( P supp ( 0g ` L ) ) ) )
245 239 240 241 244 fvdifsupp 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( P ` h ) = ( 0g ` L ) )
246 245 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) = ( ( 0g ` L ) ( .r ` L ) ( ( u ` h ) ` c ) ) )
247 21 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> L e. Ring )
248 75 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> F C_ ( Base ` L ) )
249 12 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
250 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> F e. ( SubDRing ` J ) )
251 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( F ^m B ) e. _V )
252 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> u e. ( ( F ^m B ) ^m H ) )
253 240 251 252 elmaprd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> u : H --> ( F ^m B ) )
254 253 242 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( u ` h ) e. ( F ^m B ) )
255 249 250 254 elmaprd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( u ` h ) : B --> F )
256 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> c e. B )
257 255 256 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( ( u ` h ) ` c ) e. F )
258 248 257 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( ( u ` h ) ` c ) e. ( Base ` L ) )
259 39 31 19 247 258 ringlzd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( ( 0g ` L ) ( .r ` L ) ( ( u ` h ) ` c ) ) = ( 0g ` L ) )
260 246 259 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. h e. ( P supp ( 0g ` L ) ) ) -> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) = ( 0g ` L ) )
261 12 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
262 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> F e. ( SubDRing ` J ) )
263 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> H e. ( SubDRing ` L ) )
264 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( F ^m B ) e. _V )
265 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> u e. ( ( F ^m B ) ^m H ) )
266 263 264 265 elmaprd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> u : H --> ( F ^m B ) )
267 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> h e. H )
268 266 267 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( u ` h ) e. ( F ^m B ) )
269 261 262 268 elmaprd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( u ` h ) : B --> F )
270 269 ffnd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( u ` h ) Fn B )
271 fvexd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( 0g ` L ) e. _V )
272 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> c e. B )
273 simpr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> -. c e. ( ( u ` h ) supp ( 0g ` L ) ) )
274 272 273 eldifd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> c e. ( B \ ( ( u ` h ) supp ( 0g ` L ) ) ) )
275 270 261 271 274 fvdifsupp 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( ( u ` h ) ` c ) = ( 0g ` L ) )
276 275 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) = ( ( P ` h ) ( .r ` L ) ( 0g ` L ) ) )
277 201 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> L e. Ring )
278 204 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( P ` h ) e. ( Base ` L ) )
279 39 31 19 277 278 ringrzd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( ( P ` h ) ( .r ` L ) ( 0g ` L ) ) = ( 0g ` L ) )
280 276 279 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) -> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) = ( 0g ` L ) )
281 df-br 
 |-  ( c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h <-> <. c , h >. e. U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) )
282 fveq2 
 |-  ( h = i -> ( u ` h ) = ( u ` i ) )
283 282 oveq1d 
 |-  ( h = i -> ( ( u ` h ) supp ( 0g ` L ) ) = ( ( u ` i ) supp ( 0g ` L ) ) )
284 sneq 
 |-  ( h = i -> { h } = { i } )
285 283 284 xpeq12d 
 |-  ( h = i -> ( ( ( u ` h ) supp ( 0g ` L ) ) X. { h } ) = ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) )
286 285 cbviunv 
 |-  U_ h e. ( P supp ( 0g ` L ) ) ( ( ( u ` h ) supp ( 0g ` L ) ) X. { h } ) = U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } )
287 286 eleq2i 
 |-  ( <. c , h >. e. U_ h e. ( P supp ( 0g ` L ) ) ( ( ( u ` h ) supp ( 0g ` L ) ) X. { h } ) <-> <. c , h >. e. U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) )
288 opeliun2xp 
 |-  ( <. c , h >. e. U_ h e. ( P supp ( 0g ` L ) ) ( ( ( u ` h ) supp ( 0g ` L ) ) X. { h } ) <-> ( h e. ( P supp ( 0g ` L ) ) /\ c e. ( ( u ` h ) supp ( 0g ` L ) ) ) )
289 281 287 288 3bitr2i 
 |-  ( c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h <-> ( h e. ( P supp ( 0g ` L ) ) /\ c e. ( ( u ` h ) supp ( 0g ` L ) ) ) )
290 289 notbii 
 |-  ( -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h <-> -. ( h e. ( P supp ( 0g ` L ) ) /\ c e. ( ( u ` h ) supp ( 0g ` L ) ) ) )
291 ianor 
 |-  ( -. ( h e. ( P supp ( 0g ` L ) ) /\ c e. ( ( u ` h ) supp ( 0g ` L ) ) ) <-> ( -. h e. ( P supp ( 0g ` L ) ) \/ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) )
292 290 291 sylbb 
 |-  ( -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h -> ( -. h e. ( P supp ( 0g ` L ) ) \/ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) )
293 292 adantl 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> ( -. h e. ( P supp ( 0g ` L ) ) \/ -. c e. ( ( u ` h ) supp ( 0g ` L ) ) ) )
294 260 280 293 mpjaodan 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) = ( 0g ` L ) )
295 294 oveq1d 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( ( 0g ` L ) ( .r ` L ) c ) )
296 122 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> L e. Ring )
297 207 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> c e. ( Base ` L ) )
298 39 31 19 296 297 ringlzd 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> ( ( 0g ` L ) ( .r ` L ) c ) = ( 0g ` L ) )
299 295 298 eqtrd 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( 0g ` L ) )
300 299 an42ds 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ h e. H ) /\ c e. B ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( 0g ` L ) )
301 300 an32s 
 |-  ( ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ c e. B ) /\ h e. H ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( 0g ` L ) )
302 301 anasss 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) /\ ( c e. B /\ h e. H ) ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( 0g ` L ) )
303 302 an32s 
 |-  ( ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ ( c e. B /\ h e. H ) ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( 0g ` L ) )
304 303 anasss 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ ( ( c e. B /\ h e. H ) /\ -. c U_ i e. ( P supp ( 0g ` L ) ) ( ( ( u ` i ) supp ( 0g ` L ) ) X. { i } ) h ) ) -> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) = ( 0g ` L ) )
305 39 19 200 18 158 210 237 304 gsumcom3 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( L gsum ( c e. B |-> ( L gsum ( h e. H |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) ) ) = ( L gsum ( h e. H |-> ( L gsum ( c e. B |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) ) ) )
306 195 199 305 3eqtr4d 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) ) = ( L gsum ( c e. B |-> ( L gsum ( h e. H |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) ) ) )
307 122 adantr 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> L e. Ring )
308 39 19 31 307 24 207 205 92 gsummulc1 
 |-  ( ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) /\ c e. B ) -> ( L gsum ( h e. H |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) = ( ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) ( .r ` L ) c ) )
309 308 mpteq2dva 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( c e. B |-> ( L gsum ( h e. H |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) ) = ( c e. B |-> ( ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) ( .r ` L ) c ) ) )
310 309 oveq2d 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( L gsum ( c e. B |-> ( L gsum ( h e. H |-> ( ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ( .r ` L ) c ) ) ) ) ) = ( L gsum ( c e. B |-> ( ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) ( .r ` L ) c ) ) ) )
311 121 306 310 3eqtrd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> X = ( L gsum ( c e. B |-> ( ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) ( .r ` L ) c ) ) ) )
312 60 166 oveq12d 
 |-  ( f = h -> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) = ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` b ) ) )
313 312 cbvmptv 
 |-  ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) = ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` b ) ) )
314 186 oveq2d 
 |-  ( b = c -> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` b ) ) = ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) )
315 314 mpteq2dv 
 |-  ( b = c -> ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` b ) ) ) = ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) )
316 313 315 eqtrid 
 |-  ( b = c -> ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) = ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) )
317 316 oveq2d 
 |-  ( b = c -> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) = ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) )
318 317 187 oveq12d 
 |-  ( b = c -> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) = ( ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) ( .r ` L ) c ) )
319 318 cbvmptv 
 |-  ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) = ( c e. B |-> ( ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) ( .r ` L ) c ) )
320 319 oveq2i 
 |-  ( L gsum ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) ) = ( L gsum ( c e. B |-> ( ( L gsum ( h e. H |-> ( ( P ` h ) ( .r ` L ) ( ( u ` h ) ` c ) ) ) ) ( .r ` L ) c ) ) )
321 311 320 eqtr4di 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> X = ( L gsum ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) ) )
322 120 321 jca 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> ( ( c e. B |-> ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` c ) ) ) ) ) finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) ( ( u ` f ) ` b ) ) ) ) ( .r ` L ) b ) ) ) ) )
323 96 116 322 rspcedvd 
 |-  ( ( ( ph /\ u e. ( ( F ^m B ) ^m H ) ) /\ A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) -> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) ) ) )
324 breq1 
 |-  ( e = ( u ` f ) -> ( e finSupp ( 0g ` L ) <-> ( u ` f ) finSupp ( 0g ` L ) ) )
325 fveq1 
 |-  ( e = ( u ` f ) -> ( e ` b ) = ( ( u ` f ) ` b ) )
326 325 oveq1d 
 |-  ( e = ( u ` f ) -> ( ( e ` b ) ( .r ` L ) b ) = ( ( ( u ` f ) ` b ) ( .r ` L ) b ) )
327 326 mpteq2dv 
 |-  ( e = ( u ` f ) -> ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) = ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) )
328 327 oveq2d 
 |-  ( e = ( u ` f ) -> ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) )
329 328 eqeq2d 
 |-  ( e = ( u ` f ) -> ( f = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) <-> f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) )
330 324 329 anbi12d 
 |-  ( e = ( u ` f ) -> ( ( e finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) ) <-> ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) ) )
331 ovexd 
 |-  ( ph -> ( F ^m B ) e. _V )
332 eqid 
 |-  ( LSpan ` ( ( subringAlg ` J ) ` F ) ) = ( LSpan ` ( ( subringAlg ` J ) ` F ) )
333 143 144 332 lbssp 
 |-  ( B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) -> ( ( LSpan ` ( ( subringAlg ` J ) ` F ) ) ` B ) = ( Base ` ( ( subringAlg ` J ) ` F ) ) )
334 12 333 syl 
 |-  ( ph -> ( ( LSpan ` ( ( subringAlg ` J ) ` F ) ) ` B ) = ( Base ` ( ( subringAlg ` J ) ` F ) ) )
335 148 73 334 3eqtr4rd 
 |-  ( ph -> ( ( LSpan ` ( ( subringAlg ` J ) ` F ) ) ` B ) = H )
336 335 eleq2d 
 |-  ( ph -> ( f e. ( ( LSpan ` ( ( subringAlg ` J ) ` F ) ) ` B ) <-> f e. H ) )
337 eqid 
 |-  ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) = ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) )
338 eqid 
 |-  ( Scalar ` ( ( subringAlg ` J ) ` F ) ) = ( Scalar ` ( ( subringAlg ` J ) ` F ) )
339 eqid 
 |-  ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) = ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) )
340 eqid 
 |-  ( .s ` ( ( subringAlg ` J ) ` F ) ) = ( .s ` ( ( subringAlg ` J ) ` F ) )
341 sdrgsubrg 
 |-  ( F e. ( SubDRing ` J ) -> F e. ( SubRing ` J ) )
342 6 341 syl 
 |-  ( ph -> F e. ( SubRing ` J ) )
343 eqid 
 |-  ( ( subringAlg ` J ) ` F ) = ( ( subringAlg ` J ) ` F )
344 343 sralmod 
 |-  ( F e. ( SubRing ` J ) -> ( ( subringAlg ` J ) ` F ) e. LMod )
345 342 344 syl 
 |-  ( ph -> ( ( subringAlg ` J ) ` F ) e. LMod )
346 332 143 337 338 339 340 345 146 ellspds 
 |-  ( ph -> ( f e. ( ( LSpan ` ( ( subringAlg ` J ) ` F ) ) ` B ) <-> E. e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) /\ f = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) ) ) )
347 336 346 bitr3d 
 |-  ( ph -> ( f e. H <-> E. e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) /\ f = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) ) ) )
348 347 biimpa 
 |-  ( ( ph /\ f e. H ) -> E. e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) /\ f = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) ) )
349 eqid 
 |-  ( J |`s F ) = ( J |`s F )
350 349 67 ressbas2 
 |-  ( F C_ ( Base ` J ) -> F = ( Base ` ( J |`s F ) ) )
351 69 350 syl 
 |-  ( ph -> F = ( Base ` ( J |`s F ) ) )
352 147 69 srasca 
 |-  ( ph -> ( J |`s F ) = ( Scalar ` ( ( subringAlg ` J ) ` F ) ) )
353 352 fveq2d 
 |-  ( ph -> ( Base ` ( J |`s F ) ) = ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) )
354 351 353 eqtr2d 
 |-  ( ph -> ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) = F )
355 354 oveq1d 
 |-  ( ph -> ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) = ( F ^m B ) )
356 sdrgsubrg 
 |-  ( H e. ( SubDRing ` L ) -> H e. ( SubRing ` L ) )
357 8 356 syl 
 |-  ( ph -> H e. ( SubRing ` L ) )
358 subrgsubg 
 |-  ( H e. ( SubRing ` L ) -> H e. ( SubGrp ` L ) )
359 3 19 subg0 
 |-  ( H e. ( SubGrp ` L ) -> ( 0g ` L ) = ( 0g ` J ) )
360 357 358 359 3syl 
 |-  ( ph -> ( 0g ` L ) = ( 0g ` J ) )
361 3 sdrgdrng 
 |-  ( H e. ( SubDRing ` L ) -> J e. DivRing )
362 8 361 syl 
 |-  ( ph -> J e. DivRing )
363 362 drngringd 
 |-  ( ph -> J e. Ring )
364 363 ringcmnd 
 |-  ( ph -> J e. CMnd )
365 364 cmnmndd 
 |-  ( ph -> J e. Mnd )
366 subrgsubg 
 |-  ( F e. ( SubRing ` J ) -> F e. ( SubGrp ` J ) )
367 eqid 
 |-  ( 0g ` J ) = ( 0g ` J )
368 367 subg0cl 
 |-  ( F e. ( SubGrp ` J ) -> ( 0g ` J ) e. F )
369 342 366 368 3syl 
 |-  ( ph -> ( 0g ` J ) e. F )
370 349 67 367 ress0g 
 |-  ( ( J e. Mnd /\ ( 0g ` J ) e. F /\ F C_ ( Base ` J ) ) -> ( 0g ` J ) = ( 0g ` ( J |`s F ) ) )
371 365 369 69 370 syl3anc 
 |-  ( ph -> ( 0g ` J ) = ( 0g ` ( J |`s F ) ) )
372 352 fveq2d 
 |-  ( ph -> ( 0g ` ( J |`s F ) ) = ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) )
373 360 371 372 3eqtrrd 
 |-  ( ph -> ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) = ( 0g ` L ) )
374 373 breq2d 
 |-  ( ph -> ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) <-> e finSupp ( 0g ` L ) ) )
375 374 adantr 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) <-> e finSupp ( 0g ` L ) ) )
376 12 adantr 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) ) )
377 subgsubm 
 |-  ( H e. ( SubGrp ` L ) -> H e. ( SubMnd ` L ) )
378 357 358 377 3syl 
 |-  ( ph -> H e. ( SubMnd ` L ) )
379 378 adantr 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> H e. ( SubMnd ` L ) )
380 3 31 ressmulr 
 |-  ( H e. ( SubDRing ` L ) -> ( .r ` L ) = ( .r ` J ) )
381 8 380 syl 
 |-  ( ph -> ( .r ` L ) = ( .r ` J ) )
382 147 69 sravsca 
 |-  ( ph -> ( .r ` J ) = ( .s ` ( ( subringAlg ` J ) ` F ) ) )
383 381 382 eqtrd 
 |-  ( ph -> ( .r ` L ) = ( .s ` ( ( subringAlg ` J ) ` F ) ) )
384 383 ad2antrr 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> ( .r ` L ) = ( .s ` ( ( subringAlg ` J ) ` F ) ) )
385 384 oveqd 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> ( ( e ` b ) ( .r ` L ) b ) = ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) )
386 357 ad2antrr 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> H e. ( SubRing ` L ) )
387 74 ad2antrr 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> F C_ H )
388 5 adantr 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> F e. ( SubDRing ` I ) )
389 355 eleq2d 
 |-  ( ph -> ( e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) <-> e e. ( F ^m B ) ) )
390 389 biimpa 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> e e. ( F ^m B ) )
391 376 388 390 elmaprd 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> e : B --> F )
392 391 ffvelcdmda 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> ( e ` b ) e. F )
393 387 392 sseldd 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> ( e ` b ) e. H )
394 150 adantr 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> B C_ H )
395 394 sselda 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> b e. H )
396 31 386 393 395 subrgmcld 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> ( ( e ` b ) ( .r ` L ) b ) e. H )
397 385 396 eqeltrrd 
 |-  ( ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) /\ b e. B ) -> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) e. H )
398 397 fmpttd 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) : B --> H )
399 376 379 398 3 gsumsubm 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( L gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) = ( J gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) )
400 381 382 eqtr2d 
 |-  ( ph -> ( .s ` ( ( subringAlg ` J ) ` F ) ) = ( .r ` L ) )
401 400 adantr 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( .s ` ( ( subringAlg ` J ) ` F ) ) = ( .r ` L ) )
402 401 oveqd 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) = ( ( e ` b ) ( .r ` L ) b ) )
403 402 mpteq2dv 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) = ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) )
404 403 oveq2d 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( L gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) )
405 12 mptexd 
 |-  ( ph -> ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) e. _V )
406 fvexd 
 |-  ( ph -> ( ( subringAlg ` J ) ` F ) e. _V )
407 343 405 362 406 69 gsumsra 
 |-  ( ph -> ( J gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) )
408 407 adantr 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( J gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) )
409 399 404 408 3eqtr3rd 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) )
410 409 eqeq2d 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( f = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) <-> f = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) ) )
411 375 410 anbi12d 
 |-  ( ( ph /\ e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ) -> ( ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) /\ f = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) ) <-> ( e finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) ) ) )
412 355 411 rexeqbidva 
 |-  ( ph -> ( E. e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) /\ f = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) ) <-> E. e e. ( F ^m B ) ( e finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) ) ) )
413 412 adantr 
 |-  ( ( ph /\ f e. H ) -> ( E. e e. ( ( Base ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) ^m B ) ( e finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` J ) ` F ) ) ) /\ f = ( ( ( subringAlg ` J ) ` F ) gsum ( b e. B |-> ( ( e ` b ) ( .s ` ( ( subringAlg ` J ) ` F ) ) b ) ) ) ) <-> E. e e. ( F ^m B ) ( e finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) ) ) )
414 348 413 mpbid 
 |-  ( ( ph /\ f e. H ) -> E. e e. ( F ^m B ) ( e finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( e ` b ) ( .r ` L ) b ) ) ) ) )
415 330 8 331 414 ac6mapd 
 |-  ( ph -> E. u e. ( ( F ^m B ) ^m H ) A. f e. H ( ( u ` f ) finSupp ( 0g ` L ) /\ f = ( L gsum ( b e. B |-> ( ( ( u ` f ) ` b ) ( .r ` L ) b ) ) ) ) )
416 323 415 r19.29a 
 |-  ( ph -> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L ) /\ X = ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) ) ) )