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