Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fedgmul Structured version   Visualization version   GIF version

Theorem fedgmul 31119
 Description: The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, we have [𝐸:𝐾] = [𝐸:𝐹][𝐹:𝐾]. Proposition 1.2 of [Lang], p. 224. Here (dim‘𝐴) is the degree of the extension 𝐸 of 𝐾, (dim‘𝐵) is the degree of the extension 𝐸 of 𝐹, and (dim‘𝐶) is the degree of the extension 𝐹 of 𝐾. 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.)
Hypotheses
Ref Expression
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
Ref Expression
fedgmul (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))

Proof of Theorem fedgmul
Dummy variables 𝑎 𝑐 𝑓 𝑢 𝑥 𝑦 𝑧 𝑖 𝑗 𝑤 𝑏 𝑣 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fedgmul.2 . . . . 5 (𝜑𝐹 ∈ DivRing)
2 fedgmul.4 . . . . . . . 8 (𝜑𝑈 ∈ (SubRing‘𝐸))
3 fedgmul.5 . . . . . . . . . 10 (𝜑𝑉 ∈ (SubRing‘𝐹))
4 fedgmul.f . . . . . . . . . . . 12 𝐹 = (𝐸s 𝑈)
54subsubrg 19558 . . . . . . . . . . 11 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
65biimpa 480 . . . . . . . . . 10 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
72, 3, 6syl2anc 587 . . . . . . . . 9 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
87simprd 499 . . . . . . . 8 (𝜑𝑉𝑈)
9 ressabs 16559 . . . . . . . 8 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
102, 8, 9syl2anc 587 . . . . . . 7 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
114oveq1i 7149 . . . . . . 7 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
12 fedgmul.k . . . . . . 7 𝐾 = (𝐸s 𝑉)
1310, 11, 123eqtr4g 2861 . . . . . 6 (𝜑 → (𝐹s 𝑉) = 𝐾)
14 fedgmul.3 . . . . . 6 (𝜑𝐾 ∈ DivRing)
1513, 14eqeltrd 2893 . . . . 5 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
16 fedgmul.c . . . . . 6 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17 eqid 2801 . . . . . 6 (𝐹s 𝑉) = (𝐹s 𝑉)
1816, 17sralvec 31082 . . . . 5 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
191, 15, 3, 18syl3anc 1368 . . . 4 (𝜑𝐶 ∈ LVec)
20 eqid 2801 . . . . 5 (LBasis‘𝐶) = (LBasis‘𝐶)
2120lbsex 19934 . . . 4 (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
2219, 21syl 17 . . 3 (𝜑 → (LBasis‘𝐶) ≠ ∅)
23 n0 4263 . . 3 ((LBasis‘𝐶) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
2422, 23sylib 221 . 2 (𝜑 → ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
25 fedgmul.1 . . . . . . 7 (𝜑𝐸 ∈ DivRing)
26 fedgmul.b . . . . . . . 8 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
2726, 4sralvec 31082 . . . . . . 7 ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
2825, 1, 2, 27syl3anc 1368 . . . . . 6 (𝜑𝐵 ∈ LVec)
29 eqid 2801 . . . . . . 7 (LBasis‘𝐵) = (LBasis‘𝐵)
3029lbsex 19934 . . . . . 6 (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
3128, 30syl 17 . . . . 5 (𝜑 → (LBasis‘𝐵) ≠ ∅)
32 n0 4263 . . . . 5 ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
3331, 32sylib 221 . . . 4 (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
3433adantr 484 . . 3 ((𝜑𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
35 drngring 19506 . . . . . . . . . . . . . . 15 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
3625, 35syl 17 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ Ring)
3736ad4antr 731 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝐸 ∈ Ring)
38 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
39 eqid 2801 . . . . . . . . . . . . . . . . . 18 (Base‘𝐶) = (Base‘𝐶)
4039, 20lbsss 19846 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
4138, 40syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
42 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐸) = (Base‘𝐸)
4342subrgss 19533 . . . . . . . . . . . . . . . . . . . . 21 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
442, 43syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ⊆ (Base‘𝐸))
454, 42ressbas2 16551 . . . . . . . . . . . . . . . . . . . 20 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
4644, 45syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑈 = (Base‘𝐹))
4716a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
48 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐹) = (Base‘𝐹)
4948subrgss 19533 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
503, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑉 ⊆ (Base‘𝐹))
5147, 50srabase 19947 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
5246, 51eqtrd 2836 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 = (Base‘𝐶))
5352, 44eqsstrrd 3957 . . . . . . . . . . . . . . . . 17 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
5453ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
5541, 54sstrd 3928 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
5655ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑥 ⊆ (Base‘𝐸))
57 simpr 488 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑖𝑥)
5856, 57sseldd 3919 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑖 ∈ (Base‘𝐸))
59 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
60 eqid 2801 . . . . . . . . . . . . . . . . . 18 (Base‘𝐵) = (Base‘𝐵)
6160, 29lbsss 19846 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
6259, 61syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
6326a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
6463, 44srabase 19947 . . . . . . . . . . . . . . . . 17 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
6564ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
6662, 65sseqtrrd 3959 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
6766ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑦 ⊆ (Base‘𝐸))
68 simplr 768 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑗𝑦)
6967, 68sseldd 3919 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑗 ∈ (Base‘𝐸))
70 eqid 2801 . . . . . . . . . . . . . 14 (.r𝐸) = (.r𝐸)
7142, 70ringcl 19311 . . . . . . . . . . . . 13 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
7237, 58, 69, 71syl3anc 1368 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
73 fedgmul.a . . . . . . . . . . . . . . 15 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
7473a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 = ((subringAlg ‘𝐸)‘𝑉))
757simpld 498 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (SubRing‘𝐸))
7642subrgss 19533 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
7775, 76syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐸))
7874, 77srabase 19947 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
7978ad4antr 731 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (Base‘𝐸) = (Base‘𝐴))
8072, 79eleqtrd 2895 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
8180anasss 470 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑦𝑖𝑥)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
8281ralrimivva 3159 . . . . . . . . 9 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
83 oveq2 7147 . . . . . . . . . . 11 (𝑤 = 𝑗 → (𝑡(.r𝐸)𝑤) = (𝑡(.r𝐸)𝑗))
84 oveq1 7146 . . . . . . . . . . 11 (𝑡 = 𝑖 → (𝑡(.r𝐸)𝑗) = (𝑖(.r𝐸)𝑗))
8583, 84cbvmpov 7232 . . . . . . . . . 10 (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) = (𝑗𝑦, 𝑖𝑥 ↦ (𝑖(.r𝐸)𝑗))
8685fmpo 7752 . . . . . . . . 9 (∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
8782, 86sylib 221 . . . . . . . 8 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
88 eqid 2801 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
89 eqid 2801 . . . . . . . . . . . . . 14 ( ·𝑠𝐵) = ( ·𝑠𝐵)
90 eqid 2801 . . . . . . . . . . . . . 14 (+g𝐵) = (+g𝐵)
91 eqid 2801 . . . . . . . . . . . . . 14 (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
9228ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LVec)
9392ad5antr 733 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝐵 ∈ LVec)
9429lbslinds 20526 . . . . . . . . . . . . . . . 16 (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
9594, 59sseldi 3916 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LIndS‘𝐵))
9695ad5antr 733 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑦 ∈ (LIndS‘𝐵))
9768ad3antrrr 729 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑗𝑦)
98 simpllr 775 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑣𝑦)
9963, 44srasca 19950 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
1004, 99syl5eq 2848 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 = (Scalar‘𝐵))
101100fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
102101, 51eqtr3d 2838 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
103102ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
10441, 103sseqtrrd 3959 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
105104ad5antr 733 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
106 simp-4r 783 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖𝑥)
107105, 106sseldd 3919 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
108 simplr 768 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑢𝑥)
109105, 108sseldd 3919 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
11019ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
111 eqid 2801 . . . . . . . . . . . . . . . . . . . . 21 (LSpan‘𝐶) = (LSpan‘𝐶)
11239, 20, 111islbs4 20525 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (LBasis‘𝐶) ↔ (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
11338, 112sylib 221 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
114113simpld 498 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LIndS‘𝐶))
115 eqid 2801 . . . . . . . . . . . . . . . . . . 19 (0g𝐶) = (0g𝐶)
1161150nellinds 30990 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LIndS‘𝐶)) → ¬ (0g𝐶) ∈ 𝑥)
117110, 114, 116syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ¬ (0g𝐶) ∈ 𝑥)
118117ad5antr 733 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → ¬ (0g𝐶) ∈ 𝑥)
119 nelne2 3087 . . . . . . . . . . . . . . . 16 ((𝑖𝑥 ∧ ¬ (0g𝐶) ∈ 𝑥) → 𝑖 ≠ (0g𝐶))
120106, 118, 119syl2anc 587 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g𝐶))
121100fveq2d 6653 . . . . . . . . . . . . . . . . 17 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐵)))
12216, 1, 3drgext0g 31084 . . . . . . . . . . . . . . . . 17 (𝜑 → (0g𝐹) = (0g𝐶))
123121, 122eqtr3d 2838 . . . . . . . . . . . . . . . 16 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐶))
124123ad7antr 737 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (0g‘(Scalar‘𝐵)) = (0g𝐶))
125120, 124neeqtrrd 3064 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g‘(Scalar‘𝐵)))
126 simpr 488 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢))
127 ovexd 7174 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑖(.r𝐸)𝑗) ∈ V)
12885ovmpt4g 7280 . . . . . . . . . . . . . . . . 17 ((𝑗𝑦𝑖𝑥 ∧ (𝑖(.r𝐸)𝑗) ∈ V) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑖(.r𝐸)𝑗))
12997, 106, 127, 128syl3anc 1368 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑖(.r𝐸)𝑗))
13026, 25, 2drgextvsca 31085 . . . . . . . . . . . . . . . . . 18 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
131130oveqd 7156 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑖(.r𝐸)𝑗) = (𝑖( ·𝑠𝐵)𝑗))
132131ad7antr 737 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑖(.r𝐸)𝑗) = (𝑖( ·𝑠𝐵)𝑗))
133129, 132eqtrd 2836 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑖( ·𝑠𝐵)𝑗))
13485a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) = (𝑗𝑦, 𝑖𝑥 ↦ (𝑖(.r𝐸)𝑗)))
135 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗 = 𝑣𝑖 = 𝑢)) → 𝑖 = 𝑢)
136 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗 = 𝑣𝑖 = 𝑢)) → 𝑗 = 𝑣)
137135, 136oveq12d 7157 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗 = 𝑣𝑖 = 𝑢)) → (𝑖(.r𝐸)𝑗) = (𝑢(.r𝐸)𝑣))
138 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → 𝑣𝑦)
139 simpr 488 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → 𝑢𝑥)
140 ovexd 7174 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑢(.r𝐸)𝑣) ∈ V)
141134, 137, 138, 139, 140ovmpod 7285 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
142141adantllr 718 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
143142adantl3r 749 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
144143adantr 484 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
145130oveqd 7156 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑢(.r𝐸)𝑣) = (𝑢( ·𝑠𝐵)𝑣))
146145ad7antr 737 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑢(.r𝐸)𝑣) = (𝑢( ·𝑠𝐵)𝑣))
147144, 146eqtrd 2836 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢( ·𝑠𝐵)𝑣))
148126, 133, 1473eqtr3d 2844 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑖( ·𝑠𝐵)𝑗) = (𝑢( ·𝑠𝐵)𝑣))
14988, 89, 90, 91, 93, 96, 97, 98, 107, 109, 125, 148linds2eq 30999 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗 = 𝑣𝑖 = 𝑢))
150149ex 416 . . . . . . . . . . . 12 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
151150anasss 470 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ (𝑣𝑦𝑢𝑥)) → ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
152151ralrimivva 3159 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → ∀𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
153152anasss 470 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑦𝑖𝑥)) → ∀𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
154153ralrimivva 3159 . . . . . . . 8 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗𝑦𝑖𝑥𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
155 f1opr 7193 . . . . . . . 8 ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ↔ ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴) ∧ ∀𝑗𝑦𝑖𝑥𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢))))
15687, 154, 155sylanbrc 586 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴))
15759, 38xpexd 7458 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
158 f1rnen 30392 . . . . . . 7 (((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ≈ (𝑦 × 𝑥))
159156, 157, 158syl2anc 587 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ≈ (𝑦 × 𝑥))
160 hasheni 13708 . . . . . 6 (ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
161159, 160syl 17 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
162 hashxpe 30559 . . . . . 6 ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
16359, 38, 162syl2anc 587 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
164161, 163eqtrd 2836 . . . 4 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = ((♯‘𝑦) ·e (♯‘𝑥)))
16573, 12sralvec 31082 . . . . . . 7 ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
16625, 14, 75, 165syl3anc 1368 . . . . . 6 (𝜑𝐴 ∈ LVec)
167166ad2antrr 725 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
168 lveclmod 19875 . . . . . . . . 9 (𝐴 ∈ LVec → 𝐴 ∈ LMod)
169166, 168syl 17 . . . . . . . 8 (𝜑𝐴 ∈ LMod)
170169ad2antrr 725 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LMod)
17125ad4antr 731 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝐸 ∈ DivRing)
1721ad4antr 731 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝐹 ∈ DivRing)
17314ad4antr 731 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝐾 ∈ DivRing)
1742ad4antr 731 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑈 ∈ (SubRing‘𝐸))
1753ad4antr 731 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑉 ∈ (SubRing‘𝐹))
176 fveq2 6649 . . . . . . . . . . . 12 (𝑤 = 𝑗 → (𝑓𝑤) = (𝑓𝑗))
177176fveq1d 6651 . . . . . . . . . . 11 (𝑤 = 𝑗 → ((𝑓𝑤)‘𝑣) = ((𝑓𝑗)‘𝑣))
178 fveq2 6649 . . . . . . . . . . 11 (𝑣 = 𝑖 → ((𝑓𝑗)‘𝑣) = ((𝑓𝑗)‘𝑖))
179177, 178cbvmpov 7232 . . . . . . . . . 10 (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) = (𝑗𝑦, 𝑖𝑥 ↦ ((𝑓𝑗)‘𝑖))
180 simp-4r 783 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑥 ∈ (LBasis‘𝐶))
181 simpllr 775 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑦 ∈ (LBasis‘𝐵))
182 simplr 768 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))))
183 simpr 488 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴))
18473, 26, 16, 4, 12, 171, 172, 173, 174, 175, 85, 179, 180, 181, 182, 183fedgmullem2 31118 . . . . . . . . 9 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))
185184ex 416 . . . . . . . 8 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) → ((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
186185ralrimiva 3152 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
187 eqid 2801 . . . . . . . . 9 (Base‘𝐴) = (Base‘𝐴)
188 eqid 2801 . . . . . . . . 9 (Scalar‘𝐴) = (Scalar‘𝐴)
189 eqid 2801 . . . . . . . . 9 ( ·𝑠𝐴) = ( ·𝑠𝐴)
190 eqid 2801 . . . . . . . . 9 (0g𝐴) = (0g𝐴)
191 eqid 2801 . . . . . . . . 9 (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
192 eqid 2801 . . . . . . . . 9 (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
193187, 188, 189, 190, 191, 192islindf4 20531 . . . . . . . 8 ((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) → ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴 ↔ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))))
194193biimpar 481 . . . . . . 7 (((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) ∧ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴)
195170, 157, 87, 186, 194syl31anc 1370 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴)
19672anasss 470 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑦𝑖𝑥)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
197196ralrimivva 3159 . . . . . . . . . 10 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
19885rnmposs 30441 . . . . . . . . . 10 (∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐸))
199197, 198syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐸))
20078ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐴))
201199, 200sseqtrd 3958 . . . . . . . 8 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐴))
202 eqid 2801 . . . . . . . . 9 (LSpan‘𝐴) = (LSpan‘𝐴)
203187, 202lspssv 19752 . . . . . . . 8 ((𝐴 ∈ LMod ∧ ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐴)) → ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) ⊆ (Base‘𝐴))
204170, 201, 203syl2anc 587 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) ⊆ (Base‘𝐴))
205 simpl 486 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
206205ad4antr 731 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
207 elmapi 8415 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
208207ad4antlr 732 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
209 simpr 488 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → 𝑗𝑦)
210208, 209ffvelrnd 6833 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → (𝑎𝑗) ∈ (Base‘(Scalar‘𝐵)))
211113simprd 499 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
212206, 211syl 17 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
213102ad7antr 737 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
214212, 213eqtr4d 2839 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
215210, 214eleqtrrd 2896 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → (𝑎𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
216 eqid 2801 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
217 eqid 2801 . . . . . . . . . . . . . . . . 17 (Scalar‘𝐶) = (Scalar‘𝐶)
218 eqid 2801 . . . . . . . . . . . . . . . . 17 (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
219 eqid 2801 . . . . . . . . . . . . . . . . 17 ( ·𝑠𝐶) = ( ·𝑠𝐶)
220 lveclmod 19875 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
22119, 220syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐶 ∈ LMod)
222221ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
223111, 39, 216, 217, 218, 219, 222, 41ellspds 30988 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((𝑎𝑗) ∈ ((LSpan‘𝐶)‘𝑥) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))))
224223biimpa 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑎𝑗) ∈ ((LSpan‘𝐶)‘𝑥)) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
225206, 215, 224syl2anc 587 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
226225ralrimiva 3152 . . . . . . . . . . . . 13 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) → ∀𝑗𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
227 fveq2 6649 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑗 → (𝑎𝑤) = (𝑎𝑗))
228 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝑖 → (𝑏𝑣) = (𝑏𝑖))
229 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝑖𝑣 = 𝑖)
230228, 229oveq12d 7157 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑖 → ((𝑏𝑣)( ·𝑠𝐶)𝑣) = ((𝑏𝑖)( ·𝑠𝐶)𝑖))
231230cbvmptv 5136 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)) = (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))
232231oveq2i 7150 . . . . . . . . . . . . . . . . . . 19 (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))
233232a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑗 → (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))
234227, 233eqeq12d 2817 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑗 → ((𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) ↔ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
235234anbi2d 631 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑗 → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ (𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))))
236235rexbidv 3259 . . . . . . . . . . . . . . 15 (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))))
237236cbvralvw 3399 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ ∀𝑗𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
238 vex 3447 . . . . . . . . . . . . . . 15 𝑦 ∈ V
239 breq1 5036 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑓𝑤) → (𝑏 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓𝑤) finSupp (0g‘(Scalar‘𝐶))))
240 fveq1 6648 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑓𝑤) → (𝑏𝑣) = ((𝑓𝑤)‘𝑣))
241240oveq1d 7154 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑓𝑤) → ((𝑏𝑣)( ·𝑠𝐶)𝑣) = (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))
242241mpteq2dv 5129 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑓𝑤) → (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)) = (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))
243242oveq2d 7155 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑓𝑤) → (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))
244243eqeq2d 2812 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑓𝑤) → ((𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) ↔ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))))
245239, 244anbi12d 633 . . . . . . . . . . . . . . 15 (𝑏 = (𝑓𝑤) → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))))
246238, 245ac6s 9899 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))))
247237, 246sylbir 238 . . . . . . . . . . . . 13 (∀𝑗𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))))
248226, 247syl 17 . . . . . . . . . . . 12 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))))
249 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
250 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑗𝑦)
251249, 250ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑓𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥))
252 elmapi 8415 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥) → (𝑓𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
253251, 252syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑓𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
254253anasss 470 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → (𝑓𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
255 simprr 772 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → 𝑖𝑥)
256254, 255ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
25774, 77srasca 19950 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
25812, 257syl5eq 2848 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐾 = (Scalar‘𝐴))
25947, 50srasca 19950 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
26013, 259eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐾 = (Scalar‘𝐶))
261258, 260eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
262261fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
263262ad4antr 731 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
264256, 263eleqtrrd 2896 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
265264ralrimivva 3159 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ∀𝑗𝑦𝑖𝑥 ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
266179fmpo 7752 . . . . . . . . . . . . . . . . . . 19 (∀𝑗𝑦𝑖𝑥 ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
267265, 266sylib 221 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
268 fvexd 6664 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (Base‘(Scalar‘𝐴)) ∈ V)
269157adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑦 × 𝑥) ∈ V)
270268, 269elmapd 8407 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)) ↔ (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴))))
271267, 270mpbird 260 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
272271ad5ant15 758 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
273272adantr 484 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
274273adantl3r 749 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
275 simpr 488 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣))) → 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)))
276275breq1d 5043 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣))) → (𝑐 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) finSupp (0g‘(Scalar‘𝐴))))
277275oveq1d 7154 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣))) → (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∘f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
278277oveq2d 7155 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣))) → (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (𝐴 Σg ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∘f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))))
279278eqeq2d 2812 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣))) → (𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) ↔ 𝑧 = (𝐴 Σg ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∘f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
280276, 279anbi12d 633 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑥 ∈ (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𝐸)𝑤)))))))
28125ad8antr 739 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝐸 ∈ DivRing)
2821ad8antr 739 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝐹 ∈ DivRing)
28314ad8antr 739 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝐾 ∈ DivRing)
2842ad8antr 739 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑈 ∈ (SubRing‘𝐸))
2853ad8antr 739 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑉 ∈ (SubRing‘𝐹))
28638ad6antr 735 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑥 ∈ (LBasis‘𝐶))
28759ad6antr 735 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑦 ∈ (LBasis‘𝐵))
288 simpr 488 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
289288ad5antr 733 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑧 ∈ (Base‘𝐴))
290207ad5antlr 734 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
291 simp-4r 783 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑎 finSupp (0g‘(Scalar‘𝐵)))
292 simpllr 775 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤))))
293 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑗𝑤 = 𝑗)
294227, 293oveq12d 7157 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑗 → ((𝑎𝑤)( ·𝑠𝐵)𝑤) = ((𝑎𝑗)( ·𝑠𝐵)𝑗))
295294cbvmptv 5136 . . . . . . . . . . . . . . . . 17 (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)) = (𝑗𝑦 ↦ ((𝑎𝑗)( ·𝑠𝐵)𝑗))
296295oveq2i 7150 . . . . . . . . . . . . . . . 16 (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤))) = (𝐵 Σg (𝑗𝑦 ↦ ((𝑎𝑗)( ·𝑠𝐵)𝑗)))
297292, 296eqtrdi 2852 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑧 = (𝐵 Σg (𝑗𝑦 ↦ ((𝑎𝑗)( ·𝑠𝐵)𝑗))))
298 simplr 768 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
299 simpr 488 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))))
300176breq1d 5043 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑗 → ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓𝑗) finSupp (0g‘(Scalar‘𝐶))))
301 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑖 → ((𝑓𝑤)‘𝑣) = ((𝑓𝑤)‘𝑖))
302301, 229oveq12d 7157 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑖 → (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣) = (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖))
303302cbvmptv 5136 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)) = (𝑖𝑥 ↦ (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖))
304176fveq1d 6651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑗 → ((𝑓𝑤)‘𝑖) = ((𝑓𝑗)‘𝑖))
305304oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑗 → (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖) = (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖))
306305mpteq2dv 5129 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑗 → (𝑖𝑥 ↦ (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
307303, 306syl5eq 2848 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑗 → (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)) = (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
308307oveq2d 7155 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑗 → (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
309227, 308eqeq12d 2817 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑗 → ((𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))) ↔ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
310300, 309anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑗 → (((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))) ↔ ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))))
311310cbvralvw 3399 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))) ↔ ∀𝑗𝑦 ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
312299, 311sylib 221 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → ∀𝑗𝑦 ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
313312r19.21bi 3176 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑗𝑦) → ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
314313simpld 498 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑗𝑦) → (𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)))
315313simprd 499 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑗𝑦) → (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
31673, 26, 16, 4, 12, 281, 282, 283, 284, 285, 85, 179, 286, 287, 289, 290, 291, 297, 298, 314, 315fedgmullem1 31117 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∘f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
317274, 280, 316rspcedvd 3577 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ (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𝐸)𝑤))))))
318317anasss 470 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (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𝐸)𝑤))))))
319248, 318exlimddv 1936 . . . . . . . . . . 11 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
320319anasss 470 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ (𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
321 eqid 2801 . . . . . . . . . . . . . . . . 17 (LSpan‘𝐵) = (LSpan‘𝐵)
32260, 29, 321islbs4 20525 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (LBasis‘𝐵) ↔ (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
32359, 322sylib 221 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
324323simprd 499 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
325324adantr 484 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
32678, 64eqtr3d 2838 . . . . . . . . . . . . . 14 (𝜑 → (Base‘𝐴) = (Base‘𝐵))
327326ad3antrrr 729 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
328325, 327eqtr4d 2839 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
329288, 328eleqtrrd 2896 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
330 eqid 2801 . . . . . . . . . . . . 13 (Scalar‘𝐵) = (Scalar‘𝐵)
331 lveclmod 19875 . . . . . . . . . . . . . . 15 (𝐵 ∈ LVec → 𝐵 ∈ LMod)
33228, 331syl 17 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ LMod)
333332ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
334321, 60, 88, 330, 91, 89, 333, 62ellspds 30988 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐵)‘𝑦) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤))))))
335334biimpa 480 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ ((LSpan‘𝐵)‘𝑦)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))))
336205, 329, 335syl2anc 587 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))))
337320, 336r19.29a 3251 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
338 eqid 2801 . . . . . . . . . . 11 (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
339202, 187, 338, 188, 191, 189, 87, 170, 157ellspd 20495 . . . . . . . . . 10 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))))))
340339adantr 484 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))))))
341337, 340mpbird 260 . . . . . . . 8 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))))
34287ffnd 6492 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) Fn (𝑦 × 𝑥))
343342adantr 484 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) Fn (𝑦 × 𝑥))
344 fnima 6454 . . . . . . . . . 10 ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))
345343, 344syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))
346345fveq2d 6653 . . . . . . . 8 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
347341, 346eleqtrd 2895 . . . . . . 7 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
348204, 347eqelssd 3939 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (Base‘𝐴))
349 eqid 2801 . . . . . . 7 (Base‘(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (Base‘(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))
350 drngnzr 20032 . . . . . . . . . 10 (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
35114, 350syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ NzRing)
352258, 351eqeltrrd 2894 . . . . . . . 8 (𝜑 → (Scalar‘𝐴) ∈ NzRing)
353352ad2antrr 725 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Scalar‘𝐴) ∈ NzRing)
354187, 349, 188, 189, 190, 191, 202, 170, 353, 157, 156lindflbs 30998 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ∈ (LBasis‘𝐴) ↔ ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴 ∧ ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (Base‘𝐴))))
355195, 348, 354mpbir2and 712 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ∈ (LBasis‘𝐴))
356 eqid 2801 . . . . . 6 (LBasis‘𝐴) = (LBasis‘𝐴)
357356dimval 31093 . . . . 5 ((𝐴 ∈ LVec ∧ ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
358167, 355, 357syl2anc 587 . . . 4 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
35929dimval 31093 . . . . . 6 ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
36092, 59, 359syl2anc 587 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
36120dimval 31093 . . . . . 6 ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
362110, 38, 361syl2anc 587 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
363360, 362oveq12d 7157 . . . 4 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·e (dim‘𝐶)) = ((♯‘𝑦) ·e (♯‘𝑥)))
364164, 358, 3633eqtr4d 2846 . . 3 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
36534, 364exlimddv 1936 . 2 ((𝜑𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
36624, 365exlimddv 1936 1 (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2112   ≠ wne 2990  ∀wral 3109  ∃wrex 3110  Vcvv 3444   ⊆ wss 3884  ∅c0 4246  {csn 4528   class class class wbr 5033   ↦ cmpt 5113   × cxp 5521  ran crn 5524   “ cima 5526   Fn wfn 6323  ⟶wf 6324  –1-1→wf1 6325  ‘cfv 6328  (class class class)co 7139   ∈ cmpo 7141   ∘f cof 7391   ↑m cmap 8393   ≈ cen 8493   finSupp cfsupp 8821   ·e cxmu 12498  ♯chash 13690  Basecbs 16479   ↾s cress 16480  +gcplusg 16561  .rcmulr 16562  Scalarcsca 16564   ·𝑠 cvsca 16565  0gc0g 16709   Σg cgsu 16710  Ringcrg 19294  DivRingcdr 19499  SubRingcsubrg 19528  LModclmod 19631  LSpanclspn 19740  LBasisclbs 19843  LVecclvec 19871  subringAlg csra 19937  NzRingcnzr 20027   freeLMod cfrlm 20439   LIndF clindf 20497  LIndSclinds 20498  dimcldim 31091 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-reg 9044  ax-inf2 9092  ax-ac2 9878  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-rpss 7433  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-sup 8894  df-oi 8962  df-r1 9181  df-rank 9182  df-dju 9318  df-card 9356  df-acn 9359  df-ac 9531  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-xmul 12501  df-fz 12890  df-fzo 13033  df-seq 13369  df-hash 13691  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ocomp 16582  df-ds 16583  df-hom 16585  df-cco 16586  df-0g 16711  df-gsum 16712  df-prds 16717  df-pws 16719  df-mre 16853  df-mrc 16854  df-mri 16855  df-acs 16856  df-proset 17534  df-drs 17535  df-poset 17552  df-ipo 17758  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-mhm 17952  df-submnd 17953  df-grp 18102  df-minusg 18103  df-sbg 18104  df-mulg 18221  df-subg 18272  df-ghm 18352  df-cntz 18443  df-cmn 18904  df-abl 18905  df-mgp 19237  df-ur 19249  df-ring 19296  df-oppr 19373  df-dvdsr 19391  df-unit 19392  df-invr 19422  df-drng 19501  df-subrg 19530  df-lmod 19633  df-lss 19701  df-lsp 19741  df-lmhm 19791  df-lbs 19844  df-lvec 19872  df-sra 19941  df-rgmod 19942  df-nzr 20028  df-dsmm 20425  df-frlm 20440  df-uvc 20476  df-lindf 20499  df-linds 20500  df-dim 31092 This theorem is referenced by:  extdgmul  31143
 Copyright terms: Public domain W3C validator