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 ⊢ 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑉 )
fedgmul.b ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
fedgmul.c ⊢ 𝐶 = ( ( subringAlg ‘ 𝐹 ) ‘ 𝑉 )
fedgmul.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
fedgmul.k ⊢ 𝐾 = ( 𝐸 ↾s 𝑉 )
fedgmul.1 ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
fedgmul.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
fedgmul.3 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
fedgmul.4 ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
fedgmul.5 ⊢ ( 𝜑 → 𝑉 ∈ ( SubRing ‘ 𝐹 ) )
Assertion fedgmul ( 𝜑 → ( dim ‘ 𝐴 ) = ( ( dim ‘ 𝐵 ) ·e ( dim ‘ 𝐶 ) ) )

Proof

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