Metamath Proof Explorer

Theorem fedgmul

Description: The multiplicativity formula for degrees of field extensions. Given E a field extension of F , itself a field extension of K , we have [ E : K ] = [ E : F ] [ F : K ] . Proposition 1.2 of Lang, p. 224. Here ( dimA ) is the degree of the extension E of K , ( dimB ) is the degree of the extension E of F , and ( dimC ) is the degree of the extension F of K . This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023)

Ref Expression
Hypotheses fedgmul.a 
|- A = ( ( subringAlg ` E ) ` V )
fedgmul.b 
|- B = ( ( subringAlg ` E ) ` U )
fedgmul.c 
|- C = ( ( subringAlg ` F ) ` V )
fedgmul.f 
|- F = ( E |`s U )
fedgmul.k 
|- K = ( E |`s V )
fedgmul.1 
|- ( ph -> E e. DivRing )
fedgmul.2 
|- ( ph -> F e. DivRing )
fedgmul.3 
|- ( ph -> K e. DivRing )
fedgmul.4 
|- ( ph -> U e. ( SubRing ` E ) )
fedgmul.5 
|- ( ph -> V e. ( SubRing ` F ) )
Assertion fedgmul 
|- ( ph -> ( dim ` A ) = ( ( dim ` B ) *e ( dim ` C ) ) )

Proof

Step Hyp Ref Expression
1 fedgmul.a 
 |-  A = ( ( subringAlg ` E ) ` V )
2 fedgmul.b 
 |-  B = ( ( subringAlg ` E ) ` U )
3 fedgmul.c 
 |-  C = ( ( subringAlg ` F ) ` V )
4 fedgmul.f 
 |-  F = ( E |`s U )
5 fedgmul.k 
 |-  K = ( E |`s V )
6 fedgmul.1 
 |-  ( ph -> E e. DivRing )
7 fedgmul.2 
 |-  ( ph -> F e. DivRing )
8 fedgmul.3 
 |-  ( ph -> K e. DivRing )
9 fedgmul.4 
 |-  ( ph -> U e. ( SubRing ` E ) )
10 fedgmul.5 
 |-  ( ph -> V e. ( SubRing ` F ) )
11 4 subsubrg 
 |-  ( U e. ( SubRing ` E ) -> ( V e. ( SubRing ` F ) <-> ( V e. ( SubRing ` E ) /\ V C_ U ) ) )
12 11 biimpa 
 |-  ( ( U e. ( SubRing ` E ) /\ V e. ( SubRing ` F ) ) -> ( V e. ( SubRing ` E ) /\ V C_ U ) )
13 9 10 12 syl2anc 
 |-  ( ph -> ( V e. ( SubRing ` E ) /\ V C_ U ) )
14 13 simprd 
 |-  ( ph -> V C_ U )
15 ressabs 
 |-  ( ( U e. ( SubRing ` E ) /\ V C_ U ) -> ( ( E |`s U ) |`s V ) = ( E |`s V ) )
16 9 14 15 syl2anc 
 |-  ( ph -> ( ( E |`s U ) |`s V ) = ( E |`s V ) )
17 4 oveq1i 
 |-  ( F |`s V ) = ( ( E |`s U ) |`s V )
18 16 17 5 3eqtr4g 
 |-  ( ph -> ( F |`s V ) = K )
19 18 8 eqeltrd 
 |-  ( ph -> ( F |`s V ) e. DivRing )
20 eqid 
 |-  ( F |`s V ) = ( F |`s V )
21 3 20 sralvec 
 |-  ( ( F e. DivRing /\ ( F |`s V ) e. DivRing /\ V e. ( SubRing ` F ) ) -> C e. LVec )
22 7 19 10 21 syl3anc 
 |-  ( ph -> C e. LVec )
23 eqid 
 |-  ( LBasis ` C ) = ( LBasis ` C )
24 23 lbsex 
 |-  ( C e. LVec -> ( LBasis ` C ) =/= (/) )
25 22 24 syl 
 |-  ( ph -> ( LBasis ` C ) =/= (/) )
26 n0 
 |-  ( ( LBasis ` C ) =/= (/) <-> E. x x e. ( LBasis ` C ) )
27 25 26 sylib 
 |-  ( ph -> E. x x e. ( LBasis ` C ) )
28 2 4 sralvec 
 |-  ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> B e. LVec )
29 6 7 9 28 syl3anc 
 |-  ( ph -> B e. LVec )
30 eqid 
 |-  ( LBasis ` B ) = ( LBasis ` B )
31 30 lbsex 
 |-  ( B e. LVec -> ( LBasis ` B ) =/= (/) )
32 29 31 syl 
 |-  ( ph -> ( LBasis ` B ) =/= (/) )
33 n0 
 |-  ( ( LBasis ` B ) =/= (/) <-> E. y y e. ( LBasis ` B ) )
34 32 33 sylib 
 |-  ( ph -> E. y y e. ( LBasis ` B ) )
35 34 adantr 
 |-  ( ( ph /\ x e. ( LBasis ` C ) ) -> E. y y e. ( LBasis ` B ) )
36 drngring 
 |-  ( E e. DivRing -> E e. Ring )
37 6 36 syl 
 |-  ( ph -> E e. Ring )
38 37 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> E e. Ring )
39 simplr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> x e. ( LBasis ` C ) )
40 eqid 
 |-  ( Base ` C ) = ( Base ` C )
41 40 23 lbsss 
 |-  ( x e. ( LBasis ` C ) -> x C_ ( Base ` C ) )
42 39 41 syl 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> x C_ ( Base ` C ) )
43 eqid 
 |-  ( Base ` E ) = ( Base ` E )
44 43 subrgss 
 |-  ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
45 9 44 syl 
 |-  ( ph -> U C_ ( Base ` E ) )
46 4 43 ressbas2 
 |-  ( U C_ ( Base ` E ) -> U = ( Base ` F ) )
47 45 46 syl 
 |-  ( ph -> U = ( Base ` F ) )
48 3 a1i 
 |-  ( ph -> C = ( ( subringAlg ` F ) ` V ) )
49 eqid 
 |-  ( Base ` F ) = ( Base ` F )
50 49 subrgss 
 |-  ( V e. ( SubRing ` F ) -> V C_ ( Base ` F ) )
51 10 50 syl 
 |-  ( ph -> V C_ ( Base ` F ) )
52 48 51 srabase 
 |-  ( ph -> ( Base ` F ) = ( Base ` C ) )
53 47 52 eqtrd 
 |-  ( ph -> U = ( Base ` C ) )
54 53 45 eqsstrrd 
 |-  ( ph -> ( Base ` C ) C_ ( Base ` E ) )
55 54 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( Base ` C ) C_ ( Base ` E ) )
56 42 55 sstrd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> x C_ ( Base ` E ) )
57 56 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> x C_ ( Base ` E ) )
58 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> i e. x )
59 57 58 sseldd 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> i e. ( Base ` E ) )
60 simpr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> y e. ( LBasis ` B ) )
61 eqid 
 |-  ( Base ` B ) = ( Base ` B )
62 61 30 lbsss 
 |-  ( y e. ( LBasis ` B ) -> y C_ ( Base ` B ) )
63 60 62 syl 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> y C_ ( Base ` B ) )
64 2 a1i 
 |-  ( ph -> B = ( ( subringAlg ` E ) ` U ) )
65 64 45 srabase 
 |-  ( ph -> ( Base ` E ) = ( Base ` B ) )
66 65 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( Base ` E ) = ( Base ` B ) )
67 63 66 sseqtrrd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> y C_ ( Base ` E ) )
68 67 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> y C_ ( Base ` E ) )
69 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> j e. y )
70 68 69 sseldd 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> j e. ( Base ` E ) )
71 eqid 
 |-  ( .r ` E ) = ( .r ` E )
72 43 71 ringcl 
 |-  ( ( E e. Ring /\ i e. ( Base ` E ) /\ j e. ( Base ` E ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
73 38 59 70 72 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
74 1 a1i 
 |-  ( ph -> A = ( ( subringAlg ` E ) ` V ) )
75 13 simpld 
 |-  ( ph -> V e. ( SubRing ` E ) )
76 43 subrgss 
 |-  ( V e. ( SubRing ` E ) -> V C_ ( Base ` E ) )
77 75 76 syl 
 |-  ( ph -> V C_ ( Base ` E ) )
78 74 77 srabase 
 |-  ( ph -> ( Base ` E ) = ( Base ` A ) )
79 78 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> ( Base ` E ) = ( Base ` A ) )
80 73 79 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) )
81 80 anasss 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ ( j e. y /\ i e. x ) ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) )
82 81 ralrimivva 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> A. j e. y A. i e. x ( i ( .r ` E ) j ) e. ( Base ` A ) )
83 oveq2 
 |-  ( w = j -> ( t ( .r ` E ) w ) = ( t ( .r ` E ) j ) )
84 oveq1 
 |-  ( t = i -> ( t ( .r ` E ) j ) = ( i ( .r ` E ) j ) )
85 83 84 cbvmpov 
 |-  ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) = ( j e. y , i e. x |-> ( i ( .r ` E ) j ) )
86 85 fmpo 
 |-  ( A. j e. y A. i e. x ( i ( .r ` E ) j ) e. ( Base ` A ) <-> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) --> ( Base ` A ) )
87 82 86 sylib 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) --> ( Base ` A ) )
88 eqid 
 |-  ( Base ` ( Scalar ` B ) ) = ( Base ` ( Scalar ` B ) )
89 eqid 
 |-  ( .s ` B ) = ( .s ` B )
90 eqid 
 |-  ( +g ` B ) = ( +g ` B )
91 eqid 
 |-  ( 0g ` ( Scalar ` B ) ) = ( 0g ` ( Scalar ` B ) )
92 29 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> B e. LVec )
93 92 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> B e. LVec )
94 30 lbslinds 
 |-  ( LBasis ` B ) C_ ( LIndS ` B )
95 94 60 sseldi 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> y e. ( LIndS ` B ) )
96 95 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> y e. ( LIndS ` B ) )
97 69 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> j e. y )
98 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> v e. y )
99 64 45 srasca 
 |-  ( ph -> ( E |`s U ) = ( Scalar ` B ) )
100 4 99 syl5eq 
 |-  ( ph -> F = ( Scalar ` B ) )
101 100 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` B ) ) )
102 101 52 eqtr3d 
 |-  ( ph -> ( Base ` ( Scalar ` B ) ) = ( Base ` C ) )
103 102 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( Base ` ( Scalar ` B ) ) = ( Base ` C ) )
104 42 103 sseqtrrd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> x C_ ( Base ` ( Scalar ` B ) ) )
105 104 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> x C_ ( Base ` ( Scalar ` B ) ) )
106 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> i e. x )
107 105 106 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> i e. ( Base ` ( Scalar ` B ) ) )
108 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> u e. x )
109 105 108 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> u e. ( Base ` ( Scalar ` B ) ) )
110 22 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> C e. LVec )
111 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
112 40 23 111 islbs4 
 |-  ( x e. ( LBasis ` C ) <-> ( x e. ( LIndS ` C ) /\ ( ( LSpan ` C ) ` x ) = ( Base ` C ) ) )
113 39 112 sylib 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( x e. ( LIndS ` C ) /\ ( ( LSpan ` C ) ` x ) = ( Base ` C ) ) )
114 113 simpld 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> x e. ( LIndS ` C ) )
115 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
116 115 0nellinds 
 |-  ( ( C e. LVec /\ x e. ( LIndS ` C ) ) -> -. ( 0g ` C ) e. x )
117 110 114 116 syl2anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> -. ( 0g ` C ) e. x )
118 117 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> -. ( 0g ` C ) e. x )
119 nelne2 
 |-  ( ( i e. x /\ -. ( 0g ` C ) e. x ) -> i =/= ( 0g ` C ) )
120 106 118 119 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> i =/= ( 0g ` C ) )
121 100 fveq2d 
 |-  ( ph -> ( 0g ` F ) = ( 0g ` ( Scalar ` B ) ) )
122 3 7 10 drgext0g 
 |-  ( ph -> ( 0g ` F ) = ( 0g ` C ) )
123 121 122 eqtr3d 
 |-  ( ph -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` C ) )
124 123 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` C ) )
125 120 124 neeqtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> i =/= ( 0g ` ( Scalar ` B ) ) )
126 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) )
127 ovexd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( i ( .r ` E ) j ) e. _V )
128 85 ovmpt4g 
 |-  ( ( j e. y /\ i e. x /\ ( i ( .r ` E ) j ) e. _V ) -> ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( i ( .r ` E ) j ) )
129 97 106 127 128 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( i ( .r ` E ) j ) )
130 2 6 9 drgextvsca 
 |-  ( ph -> ( .r ` E ) = ( .s ` B ) )
131 130 oveqd 
 |-  ( ph -> ( i ( .r ` E ) j ) = ( i ( .s ` B ) j ) )
132 131 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( i ( .r ` E ) j ) = ( i ( .s ` B ) j ) )
133 129 132 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( i ( .s ` B ) j ) )
134 85 a1i 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) -> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) = ( j e. y , i e. x |-> ( i ( .r ` E ) j ) ) )
135 simprr 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) /\ ( j = v /\ i = u ) ) -> i = u )
136 simprl 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) /\ ( j = v /\ i = u ) ) -> j = v )
137 135 136 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) /\ ( j = v /\ i = u ) ) -> ( i ( .r ` E ) j ) = ( u ( .r ` E ) v ) )
138 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) -> v e. y )
139 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) -> u e. x )
140 ovexd 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) -> ( u ( .r ` E ) v ) e. _V )
141 134 137 138 139 140 ovmpod 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ v e. y ) /\ u e. x ) -> ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) = ( u ( .r ` E ) v ) )
142 141 adantllr 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ i e. x ) /\ v e. y ) /\ u e. x ) -> ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) = ( u ( .r ` E ) v ) )
143 142 adantl3r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) -> ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) = ( u ( .r ` E ) v ) )
144 143 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) = ( u ( .r ` E ) v ) )
145 130 oveqd 
 |-  ( ph -> ( u ( .r ` E ) v ) = ( u ( .s ` B ) v ) )
146 145 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( u ( .r ` E ) v ) = ( u ( .s ` B ) v ) )
147 144 146 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) = ( u ( .s ` B ) v ) )
148 126 133 147 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( i ( .s ` B ) j ) = ( u ( .s ` B ) v ) )
149 88 89 90 91 93 96 97 98 107 109 125 148 linds2eq 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) /\ ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) ) -> ( j = v /\ i = u ) )
150 149 ex 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ v e. y ) /\ u e. x ) -> ( ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) -> ( j = v /\ i = u ) ) )
151 150 anasss 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) /\ ( v e. y /\ u e. x ) ) -> ( ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) -> ( j = v /\ i = u ) ) )
152 151 ralrimivva 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ j e. y ) /\ i e. x ) -> A. v e. y A. u e. x ( ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) -> ( j = v /\ i = u ) ) )
153 152 anasss 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ ( j e. y /\ i e. x ) ) -> A. v e. y A. u e. x ( ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) -> ( j = v /\ i = u ) ) )
154 153 ralrimivva 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> A. j e. y A. i e. x A. v e. y A. u e. x ( ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) -> ( j = v /\ i = u ) ) )
155 f1opr 
 |-  ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) -1-1-> ( Base ` A ) <-> ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) --> ( Base ` A ) /\ A. j e. y A. i e. x A. v e. y A. u e. x ( ( j ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) i ) = ( v ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) u ) -> ( j = v /\ i = u ) ) ) )
156 87 154 155 sylanbrc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) -1-1-> ( Base ` A ) )
157 60 39 xpexd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( y X. x ) e. _V )
158 f1rnen 
 |-  ( ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) -1-1-> ( Base ` A ) /\ ( y X. x ) e. _V ) -> ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ~~ ( y X. x ) )
159 156 157 158 syl2anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ~~ ( y X. x ) )
160 hasheni 
 |-  ( ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ~~ ( y X. x ) -> ( # ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) = ( # ` ( y X. x ) ) )
161 159 160 syl 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( # ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) = ( # ` ( y X. x ) ) )
162 hashxpe 
 |-  ( ( y e. ( LBasis ` B ) /\ x e. ( LBasis ` C ) ) -> ( # ` ( y X. x ) ) = ( ( # ` y ) *e ( # ` x ) ) )
163 60 39 162 syl2anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( # ` ( y X. x ) ) = ( ( # ` y ) *e ( # ` x ) ) )
164 161 163 eqtrd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( # ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) = ( ( # ` y ) *e ( # ` x ) ) )
165 1 5 sralvec 
 |-  ( ( E e. DivRing /\ K e. DivRing /\ V e. ( SubRing ` E ) ) -> A e. LVec )
166 6 8 75 165 syl3anc 
 |-  ( ph -> A e. LVec )
167 166 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> A e. LVec )
168 lveclmod 
 |-  ( A e. LVec -> A e. LMod )
169 166 168 syl 
 |-  ( ph -> A e. LMod )
170 169 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> A e. LMod )
171 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> E e. DivRing )
172 7 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> F e. DivRing )
173 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> K e. DivRing )
174 9 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> U e. ( SubRing ` E ) )
175 10 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> V e. ( SubRing ` F ) )
176 fveq2 
 |-  ( w = j -> ( f ` w ) = ( f ` j ) )
177 176 fveq1d 
 |-  ( w = j -> ( ( f ` w ) ` v ) = ( ( f ` j ) ` v ) )
178 fveq2 
 |-  ( v = i -> ( ( f ` j ) ` v ) = ( ( f ` j ) ` i ) )
179 177 178 cbvmpov 
 |-  ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) = ( j e. y , i e. x |-> ( ( f ` j ) ` i ) )
180 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> x e. ( LBasis ` C ) )
181 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> y e. ( LBasis ` B ) )
182 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) )
183 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) )
184 1 2 3 4 5 171 172 173 174 175 85 179 180 181 182 183 fedgmullem2 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) /\ ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) ) -> c = ( ( y X. x ) X. { ( 0g ` ( Scalar ` A ) ) } ) )
185 184 ex 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ) -> ( ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) -> c = ( ( y X. x ) X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
186 185 ralrimiva 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> A. c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ( ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) -> c = ( ( y X. x ) X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
187 eqid 
 |-  ( Base ` A ) = ( Base ` A )
188 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
189 eqid 
 |-  ( .s ` A ) = ( .s ` A )
190 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
191 eqid 
 |-  ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` A ) )
192 eqid 
 |-  ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) = ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) )
193 187 188 189 190 191 192 islindf4 
 |-  ( ( A e. LMod /\ ( y X. x ) e. _V /\ ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) --> ( Base ` A ) ) -> ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) LIndF A <-> A. c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ( ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) -> c = ( ( y X. x ) X. { ( 0g ` ( Scalar ` A ) ) } ) ) ) )
194 193 biimpar 
 |-  ( ( ( A e. LMod /\ ( y X. x ) e. _V /\ ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) : ( y X. x ) --> ( Base ` A ) ) /\ A. c e. ( Base ` ( ( Scalar ` A ) freeLMod ( y X. x ) ) ) ( ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( 0g ` A ) -> c = ( ( y X. x ) X. { ( 0g ` ( Scalar ` A ) ) } ) ) ) -> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) LIndF A )
195 170 157 87 186 194 syl31anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) LIndF A )
196 73 anasss 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ ( j e. y /\ i e. x ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
197 196 ralrimivva 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> A. j e. y A. i e. x ( i ( .r ` E ) j ) e. ( Base ` E ) )
198 85 rnmposs 
 |-  ( A. j e. y A. i e. x ( i ( .r ` E ) j ) e. ( Base ` E ) -> ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) C_ ( Base ` E ) )
199 197 198 syl 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) C_ ( Base ` E ) )
200 78 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( Base ` E ) = ( Base ` A ) )
201 199 200 sseqtrd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) C_ ( Base ` A ) )
202 eqid 
 |-  ( LSpan ` A ) = ( LSpan ` A )
203 187 202 lspssv 
 |-  ( ( A e. LMod /\ ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) C_ ( Base ` A ) ) -> ( ( LSpan ` A ) ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) C_ ( Base ` A ) )
204 170 201 203 syl2anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( ( LSpan ` A ) ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) C_ ( Base ` A ) )
205 simpl 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) )
206 205 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) )
207 elmapi 
 |-  ( a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) -> a : y --> ( Base ` ( Scalar ` B ) ) )
208 207 ad4antlr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> a : y --> ( Base ` ( Scalar ` B ) ) )
209 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> j e. y )
210 208 209 ffvelrnd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> ( a ` j ) e. ( Base ` ( Scalar ` B ) ) )
211 113 simprd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( ( LSpan ` C ) ` x ) = ( Base ` C ) )
212 206 211 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> ( ( LSpan ` C ) ` x ) = ( Base ` C ) )
213 102 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> ( Base ` ( Scalar ` B ) ) = ( Base ` C ) )
214 212 213 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> ( ( LSpan ` C ) ` x ) = ( Base ` ( Scalar ` B ) ) )
215 210 214 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> ( a ` j ) e. ( ( LSpan ` C ) ` x ) )
216 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
217 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
218 eqid 
 |-  ( 0g ` ( Scalar ` C ) ) = ( 0g ` ( Scalar ` C ) )
219 eqid 
 |-  ( .s ` C ) = ( .s ` C )
220 lveclmod 
 |-  ( C e. LVec -> C e. LMod )
221 22 220 syl 
 |-  ( ph -> C e. LMod )
222 221 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> C e. LMod )
223 111 40 216 217 218 219 222 42 ellspds 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( ( a ` j ) e. ( ( LSpan ` C ) ` x ) <-> E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) ) )
224 223 biimpa 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ ( a ` j ) e. ( ( LSpan ` C ) ` x ) ) -> E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) )
225 206 215 224 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ j e. y ) -> E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) )
226 225 ralrimiva 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) -> A. j e. y E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) )
227 fveq2 
 |-  ( w = j -> ( a ` w ) = ( a ` j ) )
228 fveq2 
 |-  ( v = i -> ( b ` v ) = ( b ` i ) )
229 id 
 |-  ( v = i -> v = i )
230 228 229 oveq12d 
 |-  ( v = i -> ( ( b ` v ) ( .s ` C ) v ) = ( ( b ` i ) ( .s ` C ) i ) )
231 230 cbvmptv 
 |-  ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) = ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) )
232 231 oveq2i 
 |-  ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) )
233 232 a1i 
 |-  ( w = j -> ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) )
234 227 233 eqeq12d 
 |-  ( w = j -> ( ( a ` w ) = ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) <-> ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) )
235 234 anbi2d 
 |-  ( w = j -> ( ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) ) <-> ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) ) )
236 235 rexbidv 
 |-  ( w = j -> ( E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) ) <-> E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) ) )
237 236 cbvralvw 
 |-  ( A. w e. y E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) ) <-> A. j e. y E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) )
238 vex 
 |-  y e. _V
239 breq1 
 |-  ( b = ( f ` w ) -> ( b finSupp ( 0g ` ( Scalar ` C ) ) <-> ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) ) )
240 fveq1 
 |-  ( b = ( f ` w ) -> ( b ` v ) = ( ( f ` w ) ` v ) )
241 240 oveq1d 
 |-  ( b = ( f ` w ) -> ( ( b ` v ) ( .s ` C ) v ) = ( ( ( f ` w ) ` v ) ( .s ` C ) v ) )
242 241 mpteq2dv 
 |-  ( b = ( f ` w ) -> ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) = ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) )
243 242 oveq2d 
 |-  ( b = ( f ` w ) -> ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) )
244 243 eqeq2d 
 |-  ( b = ( f ` w ) -> ( ( a ` w ) = ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) <-> ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) )
245 239 244 anbi12d 
 |-  ( b = ( f ` w ) -> ( ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) ) <-> ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) )
246 238 245 ac6s 
 |-  ( A. w e. y E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( b ` v ) ( .s ` C ) v ) ) ) ) -> E. f ( f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) )
247 237 246 sylbir 
 |-  ( A. j e. y E. b e. ( ( Base ` ( Scalar ` C ) ) ^m x ) ( b finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( b ` i ) ( .s ` C ) i ) ) ) ) -> E. f ( f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) )
248 226 247 syl 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) -> E. f ( f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) )
249 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ j e. y ) /\ i e. x ) -> f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) )
250 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ j e. y ) /\ i e. x ) -> j e. y )
251 249 250 ffvelrnd 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ j e. y ) /\ i e. x ) -> ( f ` j ) e. ( ( Base ` ( Scalar ` C ) ) ^m x ) )
252 elmapi 
 |-  ( ( f ` j ) e. ( ( Base ` ( Scalar ` C ) ) ^m x ) -> ( f ` j ) : x --> ( Base ` ( Scalar ` C ) ) )
253 251 252 syl 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ j e. y ) /\ i e. x ) -> ( f ` j ) : x --> ( Base ` ( Scalar ` C ) ) )
254 253 anasss 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ ( j e. y /\ i e. x ) ) -> ( f ` j ) : x --> ( Base ` ( Scalar ` C ) ) )
255 simprr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ ( j e. y /\ i e. x ) ) -> i e. x )
256 254 255 ffvelrnd 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ ( j e. y /\ i e. x ) ) -> ( ( f ` j ) ` i ) e. ( Base ` ( Scalar ` C ) ) )
257 74 77 srasca 
 |-  ( ph -> ( E |`s V ) = ( Scalar ` A ) )
258 5 257 syl5eq 
 |-  ( ph -> K = ( Scalar ` A ) )
259 48 51 srasca 
 |-  ( ph -> ( F |`s V ) = ( Scalar ` C ) )
260 18 259 eqtr3d 
 |-  ( ph -> K = ( Scalar ` C ) )
261 258 260 eqtr3d 
 |-  ( ph -> ( Scalar ` A ) = ( Scalar ` C ) )
262 261 fveq2d 
 |-  ( ph -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` C ) ) )
263 262 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ ( j e. y /\ i e. x ) ) -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` C ) ) )
264 256 263 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ ( j e. y /\ i e. x ) ) -> ( ( f ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) )
265 264 ralrimivva 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) -> A. j e. y A. i e. x ( ( f ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) )
266 179 fmpo 
 |-  ( A. j e. y A. i e. x ( ( f ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) <-> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) : ( y X. x ) --> ( Base ` ( Scalar ` A ) ) )
267 265 266 sylib 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) -> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) : ( y X. x ) --> ( Base ` ( Scalar ` A ) ) )
268 fvexd 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) -> ( Base ` ( Scalar ` A ) ) e. _V )
269 157 adantr 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) -> ( y X. x ) e. _V )
270 268 269 elmapd 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) -> ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) <-> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) : ( y X. x ) --> ( Base ` ( Scalar ` A ) ) ) )
271 267 270 mpbird 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) -> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) )
272 271 ad5ant15 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) -> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) )
273 272 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) )
274 273 adantl3r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) )
275 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ c = ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) ) -> c = ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) )
276 275 breq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ c = ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) ) -> ( c finSupp ( 0g ` ( Scalar ` A ) ) <-> ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) finSupp ( 0g ` ( Scalar ` A ) ) ) )
277 275 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ c = ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) ) -> ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) = ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) )
278 277 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ c = ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) ) -> ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) = ( A gsum ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) )
279 278 eqeq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ c = ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) ) -> ( z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) <-> z = ( A gsum ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) )
280 276 279 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ c = ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) ) -> ( ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) <-> ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) ) )
281 6 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> E e. DivRing )
282 7 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> F e. DivRing )
283 8 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> K e. DivRing )
284 9 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> U e. ( SubRing ` E ) )
285 10 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> V e. ( SubRing ` F ) )
286 39 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> x e. ( LBasis ` C ) )
287 60 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> y e. ( LBasis ` B ) )
288 simpr 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> z e. ( Base ` A ) )
289 288 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> z e. ( Base ` A ) )
290 207 ad5antlr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> a : y --> ( Base ` ( Scalar ` B ) ) )
291 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> a finSupp ( 0g ` ( Scalar ` B ) ) )
292 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) )
293 id 
 |-  ( w = j -> w = j )
294 227 293 oveq12d 
 |-  ( w = j -> ( ( a ` w ) ( .s ` B ) w ) = ( ( a ` j ) ( .s ` B ) j ) )
295 294 cbvmptv 
 |-  ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) = ( j e. y |-> ( ( a ` j ) ( .s ` B ) j ) )
296 295 oveq2i 
 |-  ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) = ( B gsum ( j e. y |-> ( ( a ` j ) ( .s ` B ) j ) ) )
297 292 296 eqtrdi 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> z = ( B gsum ( j e. y |-> ( ( a ` j ) ( .s ` B ) j ) ) ) )
298 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) )
299 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) )
300 176 breq1d 
 |-  ( w = j -> ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) <-> ( f ` j ) finSupp ( 0g ` ( Scalar ` C ) ) ) )
301 fveq2 
 |-  ( v = i -> ( ( f ` w ) ` v ) = ( ( f ` w ) ` i ) )
302 301 229 oveq12d 
 |-  ( v = i -> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) = ( ( ( f ` w ) ` i ) ( .s ` C ) i ) )
303 302 cbvmptv 
 |-  ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) = ( i e. x |-> ( ( ( f ` w ) ` i ) ( .s ` C ) i ) )
304 176 fveq1d 
 |-  ( w = j -> ( ( f ` w ) ` i ) = ( ( f ` j ) ` i ) )
305 304 oveq1d 
 |-  ( w = j -> ( ( ( f ` w ) ` i ) ( .s ` C ) i ) = ( ( ( f ` j ) ` i ) ( .s ` C ) i ) )
306 305 mpteq2dv 
 |-  ( w = j -> ( i e. x |-> ( ( ( f ` w ) ` i ) ( .s ` C ) i ) ) = ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) )
307 303 306 syl5eq 
 |-  ( w = j -> ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) = ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) )
308 307 oveq2d 
 |-  ( w = j -> ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) = ( C gsum ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) ) )
309 227 308 eqeq12d 
 |-  ( w = j -> ( ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) <-> ( a ` j ) = ( C gsum ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) ) ) )
310 300 309 anbi12d 
 |-  ( w = j -> ( ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) <-> ( ( f ` j ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) ) ) ) )
311 310 cbvralvw 
 |-  ( A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) <-> A. j e. y ( ( f ` j ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) ) ) )
312 299 311 sylib 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> A. j e. y ( ( f ` j ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) ) ) )
313 312 r19.21bi 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ j e. y ) -> ( ( f ` j ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` j ) = ( C gsum ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) ) ) )
314 313 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ j e. y ) -> ( f ` j ) finSupp ( 0g ` ( Scalar ` C ) ) )
315 313 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) /\ j e. y ) -> ( a ` j ) = ( C gsum ( i e. x |-> ( ( ( f ` j ) ` i ) ( .s ` C ) i ) ) ) )
316 1 2 3 4 5 281 282 283 284 285 85 179 286 287 289 290 291 297 298 314 315 fedgmullem1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( ( w e. y , v e. x |-> ( ( f ` w ) ` v ) ) oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) )
317 274 280 316 rspcedvd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) -> E. c e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) )
318 317 anasss 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) /\ ( f : y --> ( ( Base ` ( Scalar ` C ) ) ^m x ) /\ A. w e. y ( ( f ` w ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( a ` w ) = ( C gsum ( v e. x |-> ( ( ( f ` w ) ` v ) ( .s ` C ) v ) ) ) ) ) ) -> E. c e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) )
319 248 318 exlimddv 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ a finSupp ( 0g ` ( Scalar ` B ) ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) -> E. c e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) )
320 319 anasss 
 |-  ( ( ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) /\ a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ) /\ ( a finSupp ( 0g ` ( Scalar ` B ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) ) -> E. c e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) )
321 eqid 
 |-  ( LSpan ` B ) = ( LSpan ` B )
322 61 30 321 islbs4 
 |-  ( y e. ( LBasis ` B ) <-> ( y e. ( LIndS ` B ) /\ ( ( LSpan ` B ) ` y ) = ( Base ` B ) ) )
323 60 322 sylib 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( y e. ( LIndS ` B ) /\ ( ( LSpan ` B ) ` y ) = ( Base ` B ) ) )
324 323 simprd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( ( LSpan ` B ) ` y ) = ( Base ` B ) )
325 324 adantr 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( ( LSpan ` B ) ` y ) = ( Base ` B ) )
326 78 65 eqtr3d 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
327 326 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( Base ` A ) = ( Base ` B ) )
328 325 327 eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( ( LSpan ` B ) ` y ) = ( Base ` A ) )
329 288 328 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> z e. ( ( LSpan ` B ) ` y ) )
330 eqid 
 |-  ( Scalar ` B ) = ( Scalar ` B )
331 lveclmod 
 |-  ( B e. LVec -> B e. LMod )
332 29 331 syl 
 |-  ( ph -> B e. LMod )
333 332 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> B e. LMod )
334 321 61 88 330 91 89 333 63 ellspds 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( z e. ( ( LSpan ` B ) ` y ) <-> E. a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ( a finSupp ( 0g ` ( Scalar ` B ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) ) )
335 334 biimpa 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( ( LSpan ` B ) ` y ) ) -> E. a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ( a finSupp ( 0g ` ( Scalar ` B ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) )
336 205 329 335 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> E. a e. ( ( Base ` ( Scalar ` B ) ) ^m y ) ( a finSupp ( 0g ` ( Scalar ` B ) ) /\ z = ( B gsum ( w e. y |-> ( ( a ` w ) ( .s ` B ) w ) ) ) ) )
337 320 336 r19.29a 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> E. c e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) )
338 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
339 202 187 338 188 191 189 87 170 157 ellspd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( z e. ( ( LSpan ` A ) ` ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) " ( y X. x ) ) ) <-> E. c e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) ) )
340 339 adantr 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( z e. ( ( LSpan ` A ) ` ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) " ( y X. x ) ) ) <-> E. c e. ( ( Base ` ( Scalar ` A ) ) ^m ( y X. x ) ) ( c finSupp ( 0g ` ( Scalar ` A ) ) /\ z = ( A gsum ( c oF ( .s ` A ) ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) ) ) ) )
341 337 340 mpbird 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> z e. ( ( LSpan ` A ) ` ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) " ( y X. x ) ) ) )
342 87 ffnd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) Fn ( y X. x ) )
343 342 adantr 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) Fn ( y X. x ) )
344 fnima 
 |-  ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) Fn ( y X. x ) -> ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) " ( y X. x ) ) = ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) )
345 343 344 syl 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) " ( y X. x ) ) = ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) )
346 345 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> ( ( LSpan ` A ) ` ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) " ( y X. x ) ) ) = ( ( LSpan ` A ) ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) )
347 341 346 eleqtrd 
 |-  ( ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) /\ z e. ( Base ` A ) ) -> z e. ( ( LSpan ` A ) ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) )
348 204 347 eqelssd 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( ( LSpan ` A ) ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) = ( Base ` A ) )
349 eqid 
 |-  ( Base ` ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) = ( Base ` ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) )
350 drngnzr 
 |-  ( K e. DivRing -> K e. NzRing )
351 8 350 syl 
 |-  ( ph -> K e. NzRing )
352 258 351 eqeltrrd 
 |-  ( ph -> ( Scalar ` A ) e. NzRing )
353 352 ad2antrr 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( Scalar ` A ) e. NzRing )
354 187 349 188 189 190 191 202 170 353 157 156 lindflbs 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) e. ( LBasis ` A ) <-> ( ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) LIndF A /\ ( ( LSpan ` A ) ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) = ( Base ` A ) ) ) )
355 195 348 354 mpbir2and 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) e. ( LBasis ` A ) )
356 eqid 
 |-  ( LBasis ` A ) = ( LBasis ` A )
357 356 dimval 
 |-  ( ( A e. LVec /\ ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) e. ( LBasis ` A ) ) -> ( dim ` A ) = ( # ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) )
358 167 355 357 syl2anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( dim ` A ) = ( # ` ran ( w e. y , t e. x |-> ( t ( .r ` E ) w ) ) ) )
359 30 dimval 
 |-  ( ( B e. LVec /\ y e. ( LBasis ` B ) ) -> ( dim ` B ) = ( # ` y ) )
360 92 60 359 syl2anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( dim ` B ) = ( # ` y ) )
361 23 dimval 
 |-  ( ( C e. LVec /\ x e. ( LBasis ` C ) ) -> ( dim ` C ) = ( # ` x ) )
362 110 39 361 syl2anc 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( dim ` C ) = ( # ` x ) )
363 360 362 oveq12d 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( ( dim ` B ) *e ( dim ` C ) ) = ( ( # ` y ) *e ( # ` x ) ) )
364 164 358 363 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( LBasis ` C ) ) /\ y e. ( LBasis ` B ) ) -> ( dim ` A ) = ( ( dim ` B ) *e ( dim ` C ) ) )
365 35 364 exlimddv 
 |-  ( ( ph /\ x e. ( LBasis ` C ) ) -> ( dim ` A ) = ( ( dim ` B ) *e ( dim ` C ) ) )
366 27 365 exlimddv 
 |-  ( ph -> ( dim ` A ) = ( ( dim ` B ) *e ( dim ` C ) ) )