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) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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