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