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

Theorem fedgmul 31721
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 20061 . . . . . . . . . . 11 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
65biimpa 477 . . . . . . . . . 10 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
72, 3, 6syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
87simprd 496 . . . . . . . 8 (𝜑𝑉𝑈)
9 ressabs 16970 . . . . . . . 8 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
102, 8, 9syl2anc 584 . . . . . . 7 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
114oveq1i 7282 . . . . . . 7 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
12 fedgmul.k . . . . . . 7 𝐾 = (𝐸s 𝑉)
1310, 11, 123eqtr4g 2805 . . . . . 6 (𝜑 → (𝐹s 𝑉) = 𝐾)
14 fedgmul.3 . . . . . 6 (𝜑𝐾 ∈ DivRing)
1513, 14eqeltrd 2841 . . . . 5 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
16 fedgmul.c . . . . . 6 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17 eqid 2740 . . . . . 6 (𝐹s 𝑉) = (𝐹s 𝑉)
1816, 17sralvec 31684 . . . . 5 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
191, 15, 3, 18syl3anc 1370 . . . 4 (𝜑𝐶 ∈ LVec)
20 eqid 2740 . . . . 5 (LBasis‘𝐶) = (LBasis‘𝐶)
2120lbsex 20438 . . . 4 (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
2219, 21syl 17 . . 3 (𝜑 → (LBasis‘𝐶) ≠ ∅)
23 n0 4286 . . 3 ((LBasis‘𝐶) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
2422, 23sylib 217 . 2 (𝜑 → ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
25 fedgmul.1 . . . . . . 7 (𝜑𝐸 ∈ DivRing)
26 fedgmul.b . . . . . . . 8 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
2726, 4sralvec 31684 . . . . . . 7 ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
2825, 1, 2, 27syl3anc 1370 . . . . . 6 (𝜑𝐵 ∈ LVec)
29 eqid 2740 . . . . . . 7 (LBasis‘𝐵) = (LBasis‘𝐵)
3029lbsex 20438 . . . . . 6 (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
3128, 30syl 17 . . . . 5 (𝜑 → (LBasis‘𝐵) ≠ ∅)
32 n0 4286 . . . . 5 ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
3331, 32sylib 217 . . . 4 (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
3433adantr 481 . . 3 ((𝜑𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
35 drngring 20009 . . . . . . . . . . . . . . 15 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
3625, 35syl 17 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ Ring)
3736ad4antr 729 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝐸 ∈ Ring)
38 simplr 766 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
39 eqid 2740 . . . . . . . . . . . . . . . . . 18 (Base‘𝐶) = (Base‘𝐶)
4039, 20lbsss 20350 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
4138, 40syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
42 eqid 2740 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐸) = (Base‘𝐸)
4342subrgss 20036 . . . . . . . . . . . . . . . . . . . . 21 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
442, 43syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ⊆ (Base‘𝐸))
454, 42ressbas2 16960 . . . . . . . . . . . . . . . . . . . 20 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
4644, 45syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑈 = (Base‘𝐹))
4716a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
48 eqid 2740 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐹) = (Base‘𝐹)
4948subrgss 20036 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
503, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑉 ⊆ (Base‘𝐹))
5147, 50srabase 20452 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
5246, 51eqtrd 2780 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 = (Base‘𝐶))
5352, 44eqsstrrd 3965 . . . . . . . . . . . . . . . . 17 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
5453ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
5541, 54sstrd 3936 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
5655ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑥 ⊆ (Base‘𝐸))
57 simpr 485 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑖𝑥)
5856, 57sseldd 3927 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑖 ∈ (Base‘𝐸))
59 simpr 485 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
60 eqid 2740 . . . . . . . . . . . . . . . . . 18 (Base‘𝐵) = (Base‘𝐵)
6160, 29lbsss 20350 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
6259, 61syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
6326a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
6463, 44srabase 20452 . . . . . . . . . . . . . . . . 17 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
6564ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
6662, 65sseqtrrd 3967 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
6766ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑦 ⊆ (Base‘𝐸))
68 simplr 766 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑗𝑦)
6967, 68sseldd 3927 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑗 ∈ (Base‘𝐸))
70 eqid 2740 . . . . . . . . . . . . . 14 (.r𝐸) = (.r𝐸)
7142, 70ringcl 19811 . . . . . . . . . . . . 13 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
7237, 58, 69, 71syl3anc 1370 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
73 fedgmul.a . . . . . . . . . . . . . . 15 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
7473a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 = ((subringAlg ‘𝐸)‘𝑉))
757simpld 495 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (SubRing‘𝐸))
7642subrgss 20036 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
7775, 76syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐸))
7874, 77srabase 20452 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
7978ad4antr 729 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (Base‘𝐸) = (Base‘𝐴))
8072, 79eleqtrd 2843 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
8180anasss 467 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑦𝑖𝑥)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
8281ralrimivva 3117 . . . . . . . . 9 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
83 oveq2 7280 . . . . . . . . . . 11 (𝑤 = 𝑗 → (𝑡(.r𝐸)𝑤) = (𝑡(.r𝐸)𝑗))
84 oveq1 7279 . . . . . . . . . . 11 (𝑡 = 𝑖 → (𝑡(.r𝐸)𝑗) = (𝑖(.r𝐸)𝑗))
8583, 84cbvmpov 7365 . . . . . . . . . 10 (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) = (𝑗𝑦, 𝑖𝑥 ↦ (𝑖(.r𝐸)𝑗))
8685fmpo 7902 . . . . . . . . 9 (∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
8782, 86sylib 217 . . . . . . . 8 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
88 eqid 2740 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
89 eqid 2740 . . . . . . . . . . . . . 14 ( ·𝑠𝐵) = ( ·𝑠𝐵)
90 eqid 2740 . . . . . . . . . . . . . 14 (+g𝐵) = (+g𝐵)
91 eqid 2740 . . . . . . . . . . . . . 14 (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
9228ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LVec)
9392ad5antr 731 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝐵 ∈ LVec)
9429lbslinds 21051 . . . . . . . . . . . . . . . 16 (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
9594, 59sselid 3924 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LIndS‘𝐵))
9695ad5antr 731 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑦 ∈ (LIndS‘𝐵))
9768ad3antrrr 727 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑗𝑦)
98 simpllr 773 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑣𝑦)
9963, 44srasca 20458 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
1004, 99eqtrid 2792 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 = (Scalar‘𝐵))
101100fveq2d 6775 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
102101, 51eqtr3d 2782 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
103102ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
10441, 103sseqtrrd 3967 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
105104ad5antr 731 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
106 simp-4r 781 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖𝑥)
107105, 106sseldd 3927 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
108 simplr 766 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑢𝑥)
109105, 108sseldd 3927 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
11019ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
111 eqid 2740 . . . . . . . . . . . . . . . . . . . . 21 (LSpan‘𝐶) = (LSpan‘𝐶)
11239, 20, 111islbs4 21050 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (LBasis‘𝐶) ↔ (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
11338, 112sylib 217 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
114113simpld 495 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LIndS‘𝐶))
115 eqid 2740 . . . . . . . . . . . . . . . . . . 19 (0g𝐶) = (0g𝐶)
1161150nellinds 31575 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LIndS‘𝐶)) → ¬ (0g𝐶) ∈ 𝑥)
117110, 114, 116syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ¬ (0g𝐶) ∈ 𝑥)
118117ad5antr 731 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → ¬ (0g𝐶) ∈ 𝑥)
119 nelne2 3044 . . . . . . . . . . . . . . . 16 ((𝑖𝑥 ∧ ¬ (0g𝐶) ∈ 𝑥) → 𝑖 ≠ (0g𝐶))
120106, 118, 119syl2anc 584 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g𝐶))
121100fveq2d 6775 . . . . . . . . . . . . . . . . 17 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐵)))
12216, 1, 3drgext0g 31686 . . . . . . . . . . . . . . . . 17 (𝜑 → (0g𝐹) = (0g𝐶))
123121, 122eqtr3d 2782 . . . . . . . . . . . . . . . 16 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐶))
124123ad7antr 735 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (0g‘(Scalar‘𝐵)) = (0g𝐶))
125120, 124neeqtrrd 3020 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g‘(Scalar‘𝐵)))
126 simpr 485 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢))
127 ovexd 7307 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑖(.r𝐸)𝑗) ∈ V)
12885ovmpt4g 7415 . . . . . . . . . . . . . . . . 17 ((𝑗𝑦𝑖𝑥 ∧ (𝑖(.r𝐸)𝑗) ∈ V) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑖(.r𝐸)𝑗))
12997, 106, 127, 128syl3anc 1370 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑖(.r𝐸)𝑗))
13026, 25, 2drgextvsca 31687 . . . . . . . . . . . . . . . . . 18 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
131130oveqd 7289 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑖(.r𝐸)𝑗) = (𝑖( ·𝑠𝐵)𝑗))
132131ad7antr 735 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑖(.r𝐸)𝑗) = (𝑖( ·𝑠𝐵)𝑗))
133129, 132eqtrd 2780 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑖( ·𝑠𝐵)𝑗))
13485a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) = (𝑗𝑦, 𝑖𝑥 ↦ (𝑖(.r𝐸)𝑗)))
135 simprr 770 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗 = 𝑣𝑖 = 𝑢)) → 𝑖 = 𝑢)
136 simprl 768 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗 = 𝑣𝑖 = 𝑢)) → 𝑗 = 𝑣)
137135, 136oveq12d 7290 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗 = 𝑣𝑖 = 𝑢)) → (𝑖(.r𝐸)𝑗) = (𝑢(.r𝐸)𝑣))
138 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → 𝑣𝑦)
139 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → 𝑢𝑥)
140 ovexd 7307 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑢(.r𝐸)𝑣) ∈ V)
141134, 137, 138, 139, 140ovmpod 7420 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
142141adantllr 716 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
143142adantl3r 747 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
144143adantr 481 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢(.r𝐸)𝑣))
145130oveqd 7289 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑢(.r𝐸)𝑣) = (𝑢( ·𝑠𝐵)𝑣))
146145ad7antr 735 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑢(.r𝐸)𝑣) = (𝑢( ·𝑠𝐵)𝑣))
147144, 146eqtrd 2780 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) = (𝑢( ·𝑠𝐵)𝑣))
148126, 133, 1473eqtr3d 2788 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑖( ·𝑠𝐵)𝑗) = (𝑢( ·𝑠𝐵)𝑣))
14988, 89, 90, 91, 93, 96, 97, 98, 107, 109, 125, 148linds2eq 31584 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) ∧ (𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢)) → (𝑗 = 𝑣𝑖 = 𝑢))
150149ex 413 . . . . . . . . . . . 12 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ 𝑣𝑦) ∧ 𝑢𝑥) → ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
151150anasss 467 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) ∧ (𝑣𝑦𝑢𝑥)) → ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
152151ralrimivva 3117 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → ∀𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
153152anasss 467 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑦𝑖𝑥)) → ∀𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
154153ralrimivva 3117 . . . . . . . 8 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗𝑦𝑖𝑥𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢)))
155 f1opr 7326 . . . . . . . 8 ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ↔ ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴) ∧ ∀𝑗𝑦𝑖𝑥𝑣𝑦𝑢𝑥 ((𝑗(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑖) = (𝑣(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))𝑢) → (𝑗 = 𝑣𝑖 = 𝑢))))
15687, 154, 155sylanbrc 583 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴))
15759, 38xpexd 7596 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
158 f1rnen 30973 . . . . . . 7 (((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ≈ (𝑦 × 𝑥))
159156, 157, 158syl2anc 584 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ≈ (𝑦 × 𝑥))
160 hasheni 14073 . . . . . 6 (ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
161159, 160syl 17 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
162 hashxpe 31136 . . . . . 6 ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
16359, 38, 162syl2anc 584 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
164161, 163eqtrd 2780 . . . 4 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = ((♯‘𝑦) ·e (♯‘𝑥)))
16573, 12sralvec 31684 . . . . . . 7 ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
16625, 14, 75, 165syl3anc 1370 . . . . . 6 (𝜑𝐴 ∈ LVec)
167166ad2antrr 723 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
168 lveclmod 20379 . . . . . . . . 9 (𝐴 ∈ LVec → 𝐴 ∈ LMod)
169166, 168syl 17 . . . . . . . 8 (𝜑𝐴 ∈ LMod)
170169ad2antrr 723 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LMod)
17125ad4antr 729 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝐸 ∈ DivRing)
1721ad4antr 729 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝐹 ∈ DivRing)
17314ad4antr 729 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝐾 ∈ DivRing)
1742ad4antr 729 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑈 ∈ (SubRing‘𝐸))
1753ad4antr 729 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑉 ∈ (SubRing‘𝐹))
176 fveq2 6771 . . . . . . . . . . . 12 (𝑤 = 𝑗 → (𝑓𝑤) = (𝑓𝑗))
177176fveq1d 6773 . . . . . . . . . . 11 (𝑤 = 𝑗 → ((𝑓𝑤)‘𝑣) = ((𝑓𝑗)‘𝑣))
178 fveq2 6771 . . . . . . . . . . 11 (𝑣 = 𝑖 → ((𝑓𝑗)‘𝑣) = ((𝑓𝑗)‘𝑖))
179177, 178cbvmpov 7365 . . . . . . . . . 10 (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) = (𝑗𝑦, 𝑖𝑥 ↦ ((𝑓𝑗)‘𝑖))
180 simp-4r 781 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑥 ∈ (LBasis‘𝐶))
181 simpllr 773 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑦 ∈ (LBasis‘𝐵))
182 simplr 766 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))))
183 simpr 485 . . . . . . . . . 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 31720 . . . . . . . . 9 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴)) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))
185184ex 413 . . . . . . . 8 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) → ((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
186185ralrimiva 3110 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
187 eqid 2740 . . . . . . . . 9 (Base‘𝐴) = (Base‘𝐴)
188 eqid 2740 . . . . . . . . 9 (Scalar‘𝐴) = (Scalar‘𝐴)
189 eqid 2740 . . . . . . . . 9 ( ·𝑠𝐴) = ( ·𝑠𝐴)
190 eqid 2740 . . . . . . . . 9 (0g𝐴) = (0g𝐴)
191 eqid 2740 . . . . . . . . 9 (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
192 eqid 2740 . . . . . . . . 9 (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
193187, 188, 189, 190, 191, 192islindf4 21056 . . . . . . . 8 ((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) → ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴 ↔ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))))
194193biimpar 478 . . . . . . 7 (((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) ∧ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))) = (0g𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴)
195170, 157, 87, 186, 194syl31anc 1372 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴)
19672anasss 467 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑦𝑖𝑥)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
197196ralrimivva 3117 . . . . . . . . . 10 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
19885rnmposs 31020 . . . . . . . . . 10 (∀𝑗𝑦𝑖𝑥 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐸))
199197, 198syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐸))
20078ad2antrr 723 . . . . . . . . 9 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐴))
201199, 200sseqtrd 3966 . . . . . . . 8 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐴))
202 eqid 2740 . . . . . . . . 9 (LSpan‘𝐴) = (LSpan‘𝐴)
203187, 202lspssv 20256 . . . . . . . 8 ((𝐴 ∈ LMod ∧ ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ⊆ (Base‘𝐴)) → ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) ⊆ (Base‘𝐴))
204170, 201, 203syl2anc 584 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) ⊆ (Base‘𝐴))
205 simpl 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
206205ad4antr 729 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
207 elmapi 8629 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
208207ad4antlr 730 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
209 simpr 485 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → 𝑗𝑦)
210208, 209ffvelrnd 6959 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → (𝑎𝑗) ∈ (Base‘(Scalar‘𝐵)))
211113simprd 496 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
212206, 211syl 17 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
213102ad7antr 735 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
214212, 213eqtr4d 2783 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
215210, 214eleqtrrd 2844 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → (𝑎𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
216 eqid 2740 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
217 eqid 2740 . . . . . . . . . . . . . . . . 17 (Scalar‘𝐶) = (Scalar‘𝐶)
218 eqid 2740 . . . . . . . . . . . . . . . . 17 (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
219 eqid 2740 . . . . . . . . . . . . . . . . 17 ( ·𝑠𝐶) = ( ·𝑠𝐶)
220 lveclmod 20379 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
22119, 220syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐶 ∈ LMod)
222221ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
223111, 39, 216, 217, 218, 219, 222, 41ellspds 31573 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((𝑎𝑗) ∈ ((LSpan‘𝐶)‘𝑥) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))))
224223biimpa 477 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑎𝑗) ∈ ((LSpan‘𝐶)‘𝑥)) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
225206, 215, 224syl2anc 584 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑗𝑦) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
226225ralrimiva 3110 . . . . . . . . . . . . 13 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) → ∀𝑗𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
227 fveq2 6771 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑗 → (𝑎𝑤) = (𝑎𝑗))
228 fveq2 6771 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝑖 → (𝑏𝑣) = (𝑏𝑖))
229 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝑖𝑣 = 𝑖)
230228, 229oveq12d 7290 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑖 → ((𝑏𝑣)( ·𝑠𝐶)𝑣) = ((𝑏𝑖)( ·𝑠𝐶)𝑖))
231230cbvmptv 5192 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)) = (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))
232231oveq2i 7283 . . . . . . . . . . . . . . . . . . 19 (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))
233232a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑗 → (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))
234227, 233eqeq12d 2756 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑗 → ((𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) ↔ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
235234anbi2d 629 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑗 → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ (𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))))
236235rexbidv 3228 . . . . . . . . . . . . . . 15 (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖))))))
237236cbvralvw 3381 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ ∀𝑗𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ ((𝑏𝑖)( ·𝑠𝐶)𝑖)))))
238 vex 3435 . . . . . . . . . . . . . . 15 𝑦 ∈ V
239 breq1 5082 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑓𝑤) → (𝑏 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓𝑤) finSupp (0g‘(Scalar‘𝐶))))
240 fveq1 6770 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑓𝑤) → (𝑏𝑣) = ((𝑓𝑤)‘𝑣))
241240oveq1d 7287 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑓𝑤) → ((𝑏𝑣)( ·𝑠𝐶)𝑣) = (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))
242241mpteq2dv 5181 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑓𝑤) → (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)) = (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))
243242oveq2d 7288 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑓𝑤) → (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))
244243eqeq2d 2751 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑓𝑤) → ((𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣))) ↔ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))))
245239, 244anbi12d 631 . . . . . . . . . . . . . . 15 (𝑏 = (𝑓𝑤) → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) ↔ ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))))
246238, 245ac6s 10251 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ ((𝑏𝑣)( ·𝑠𝐶)𝑣)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))))
247237, 246sylbir 234 . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
250 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → 𝑗𝑦)
251249, 250ffvelrnd 6959 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑓𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥))
252 elmapi 8629 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥) → (𝑓𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
253251, 252syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗𝑦) ∧ 𝑖𝑥) → (𝑓𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
254253anasss 467 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → (𝑓𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
255 simprr 770 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → 𝑖𝑥)
256254, 255ffvelrnd 6959 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
25774, 77srasca 20458 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
25812, 257eqtrid 2792 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐾 = (Scalar‘𝐴))
25947, 50srasca 20458 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
26013, 259eqtr3d 2782 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐾 = (Scalar‘𝐶))
261258, 260eqtr3d 2782 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
262261fveq2d 6775 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
263262ad4antr 729 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
264256, 263eleqtrrd 2844 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗𝑦𝑖𝑥)) → ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
265264ralrimivva 3117 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ∀𝑗𝑦𝑖𝑥 ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
266179fmpo 7902 . . . . . . . . . . . . . . . . . . 19 (∀𝑗𝑦𝑖𝑥 ((𝑓𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
267265, 266sylib 217 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
268 fvexd 6786 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (Base‘(Scalar‘𝐴)) ∈ V)
269157adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑦 × 𝑥) ∈ V)
270268, 269elmapd 8621 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)) ↔ (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴))))
271267, 270mpbird 256 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
272271ad5ant15 756 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
273272adantr 481 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
274273adantl3r 747 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
275 simpr 485 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣))) → 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)))
276275breq1d 5089 . . . . . . . . . . . . . . 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 7287 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑐 = (𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣))) → (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = ((𝑤𝑦, 𝑣𝑥 ↦ ((𝑓𝑤)‘𝑣)) ∘f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
278277oveq2d 7288 . . . . . . . . . . . . . . . 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 2751 . . . . . . . . . . . . . . 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 631 . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝐸 ∈ DivRing)
2821ad8antr 737 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝐹 ∈ DivRing)
28314ad8antr 737 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝐾 ∈ DivRing)
2842ad8antr 737 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑈 ∈ (SubRing‘𝐸))
2853ad8antr 737 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑉 ∈ (SubRing‘𝐹))
28638ad6antr 733 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑥 ∈ (LBasis‘𝐶))
28759ad6antr 733 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑦 ∈ (LBasis‘𝐵))
288 simpr 485 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
289288ad5antr 731 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑧 ∈ (Base‘𝐴))
290207ad5antlr 732 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
291 simp-4r 781 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑎 finSupp (0g‘(Scalar‘𝐵)))
292 simpllr 773 . . . . . . . . . . . . . . . 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 7290 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑗 → ((𝑎𝑤)( ·𝑠𝐵)𝑤) = ((𝑎𝑗)( ·𝑠𝐵)𝑗))
295294cbvmptv 5192 . . . . . . . . . . . . . . . . 17 (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)) = (𝑗𝑦 ↦ ((𝑎𝑗)( ·𝑠𝐵)𝑗))
296295oveq2i 7283 . . . . . . . . . . . . . . . 16 (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤))) = (𝐵 Σg (𝑗𝑦 ↦ ((𝑎𝑗)( ·𝑠𝐵)𝑗)))
297292, 296eqtrdi 2796 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑧 = (𝐵 Σg (𝑗𝑦 ↦ ((𝑎𝑗)( ·𝑠𝐵)𝑗))))
298 simplr 766 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
299 simpr 485 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))))
300176breq1d 5089 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑗 → ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓𝑗) finSupp (0g‘(Scalar‘𝐶))))
301 fveq2 6771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑖 → ((𝑓𝑤)‘𝑣) = ((𝑓𝑤)‘𝑖))
302301, 229oveq12d 7290 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑖 → (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣) = (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖))
303302cbvmptv 5192 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)) = (𝑖𝑥 ↦ (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖))
304176fveq1d 6773 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑗 → ((𝑓𝑤)‘𝑖) = ((𝑓𝑗)‘𝑖))
305304oveq1d 7287 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑗 → (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖) = (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖))
306305mpteq2dv 5181 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑗 → (𝑖𝑥 ↦ (((𝑓𝑤)‘𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
307303, 306eqtrid 2792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑗 → (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)) = (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
308307oveq2d 7288 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑗 → (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
309227, 308eqeq12d 2756 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑗 → ((𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))) ↔ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
310300, 309anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑗 → (((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))) ↔ ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))))
311310cbvralvw 3381 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣)))) ↔ ∀𝑗𝑦 ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
312299, 311sylib 217 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) → ∀𝑗𝑦 ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
313312r19.21bi 3135 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑗𝑦) → ((𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑗) = (𝐶 Σg (𝑖𝑥 ↦ (((𝑓𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))))
314313simpld 495 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤𝑦 ((𝑓𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎𝑤) = (𝐶 Σg (𝑣𝑥 ↦ (((𝑓𝑤)‘𝑣)( ·𝑠𝐶)𝑣))))) ∧ 𝑗𝑦) → (𝑓𝑗) finSupp (0g‘(Scalar‘𝐶)))
315313simprd 496 . . . . . . . . . . . . . . 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 31719 . . . . . . . . . . . . . 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 3564 . . . . . . . . . . . . 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 467 . . . . . . . . . . . 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 1942 . . . . . . . . . . 11 (((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
320319anasss 467 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ (𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
321 eqid 2740 . . . . . . . . . . . . . . . . 17 (LSpan‘𝐵) = (LSpan‘𝐵)
32260, 29, 321islbs4 21050 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (LBasis‘𝐵) ↔ (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
32359, 322sylib 217 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
324323simprd 496 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
325324adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
32678, 64eqtr3d 2782 . . . . . . . . . . . . . 14 (𝜑 → (Base‘𝐴) = (Base‘𝐵))
327326ad3antrrr 727 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
328325, 327eqtr4d 2783 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
329288, 328eleqtrrd 2844 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
330 eqid 2740 . . . . . . . . . . . . 13 (Scalar‘𝐵) = (Scalar‘𝐵)
331 lveclmod 20379 . . . . . . . . . . . . . . 15 (𝐵 ∈ LVec → 𝐵 ∈ LMod)
33228, 331syl 17 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ LMod)
333332ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
334321, 60, 88, 330, 91, 89, 333, 62ellspds 31573 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐵)‘𝑦) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤))))))
335334biimpa 477 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ ((LSpan‘𝐵)‘𝑦)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))))
336205, 329, 335syl2anc 584 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤𝑦 ↦ ((𝑎𝑤)( ·𝑠𝐵)𝑤)))))
337320, 336r19.29a 3220 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))))
338 eqid 2740 . . . . . . . . . . 11 (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
339202, 187, 338, 188, 191, 189, 87, 170, 157ellspd 21020 . . . . . . . . . 10 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))))))
340339adantr 481 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐f ( ·𝑠𝐴)(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))))))
341337, 340mpbird 256 . . . . . . . 8 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))))
34287ffnd 6599 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) Fn (𝑦 × 𝑥))
343342adantr 481 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) Fn (𝑦 × 𝑥))
344 fnima 6561 . . . . . . . . . 10 ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))
345343, 344syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))
346345fveq2d 6775 . . . . . . . 8 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
347341, 346eleqtrd 2843 . . . . . . 7 ((((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
348204, 347eqelssd 3947 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (Base‘𝐴))
349 eqid 2740 . . . . . . 7 (Base‘(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (Base‘(𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)))
350 drngnzr 20544 . . . . . . . . . 10 (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
35114, 350syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ NzRing)
352258, 351eqeltrrd 2842 . . . . . . . 8 (𝜑 → (Scalar‘𝐴) ∈ NzRing)
353352ad2antrr 723 . . . . . . 7 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Scalar‘𝐴) ∈ NzRing)
354187, 349, 188, 189, 190, 191, 202, 170, 353, 157, 156lindflbs 31583 . . . . . 6 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ∈ (LBasis‘𝐴) ↔ ((𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) LIndF 𝐴 ∧ ((LSpan‘𝐴)‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))) = (Base‘𝐴))))
355195, 348, 354mpbir2and 710 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ∈ (LBasis‘𝐴))
356 eqid 2740 . . . . . 6 (LBasis‘𝐴) = (LBasis‘𝐴)
357356dimval 31695 . . . . 5 ((𝐴 ∈ LVec ∧ ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
358167, 355, 357syl2anc 584 . . . 4 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤𝑦, 𝑡𝑥 ↦ (𝑡(.r𝐸)𝑤))))
35929dimval 31695 . . . . . 6 ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
36092, 59, 359syl2anc 584 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
36120dimval 31695 . . . . . 6 ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
362110, 38, 361syl2anc 584 . . . . 5 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
363360, 362oveq12d 7290 . . . 4 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·e (dim‘𝐶)) = ((♯‘𝑦) ·e (♯‘𝑥)))
364164, 358, 3633eqtr4d 2790 . . 3 (((𝜑𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
36534, 364exlimddv 1942 . 2 ((𝜑𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
36624, 365exlimddv 1942 1 (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wex 1786  wcel 2110  wne 2945  wral 3066  wrex 3067  Vcvv 3431  wss 3892  c0 4262  {csn 4567   class class class wbr 5079  cmpt 5162   × cxp 5588  ran crn 5591  cima 5593   Fn wfn 6427  wf 6428  1-1wf1 6429  cfv 6432  (class class class)co 7272  cmpo 7274  f cof 7526  m cmap 8607  cen 8722   finSupp cfsupp 9116   ·e cxmu 12858  chash 14055  Basecbs 16923  s cress 16952  +gcplusg 16973  .rcmulr 16974  Scalarcsca 16976   ·𝑠 cvsca 16977  0gc0g 17161   Σg cgsu 17162  Ringcrg 19794  DivRingcdr 20002  SubRingcsubrg 20031  LModclmod 20134  LSpanclspn 20244  LBasisclbs 20347  LVecclvec 20375  subringAlg csra 20441  NzRingcnzr 20539   freeLMod cfrlm 20964   LIndF clindf 21022  LIndSclinds 21023  dimcldim 31693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7583  ax-reg 9339  ax-inf2 9387  ax-ac2 10230  ax-cnex 10938  ax-resscn 10939  ax-1cn 10940  ax-icn 10941  ax-addcl 10942  ax-addrcl 10943  ax-mulcl 10944  ax-mulrcl 10945  ax-mulcom 10946  ax-addass 10947  ax-mulass 10948  ax-distr 10949  ax-i2m1 10950  ax-1ne0 10951  ax-1rid 10952  ax-rnegex 10953  ax-rrecex 10954  ax-cnre 10955  ax-pre-lttri 10956  ax-pre-lttrn 10957  ax-pre-ltadd 10958  ax-pre-mulgt0 10959
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-iin 4933  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-isom 6441  df-riota 7229  df-ov 7275  df-oprab 7276  df-mpo 7277  df-of 7528  df-rpss 7571  df-om 7708  df-1st 7825  df-2nd 7826  df-supp 7970  df-tpos 8034  df-frecs 8089  df-wrecs 8120  df-recs 8194  df-rdg 8233  df-1o 8289  df-oadd 8293  df-er 8490  df-map 8609  df-ixp 8678  df-en 8726  df-dom 8727  df-sdom 8728  df-fin 8729  df-fsupp 9117  df-sup 9189  df-oi 9257  df-r1 9533  df-rank 9534  df-dju 9670  df-card 9708  df-acn 9711  df-ac 9883  df-pnf 11022  df-mnf 11023  df-xr 11024  df-ltxr 11025  df-le 11026  df-sub 11218  df-neg 11219  df-nn 11985  df-2 12047  df-3 12048  df-4 12049  df-5 12050  df-6 12051  df-7 12052  df-8 12053  df-9 12054  df-n0 12245  df-xnn0 12317  df-z 12331  df-dec 12449  df-uz 12594  df-xmul 12861  df-fz 13251  df-fzo 13394  df-seq 13733  df-hash 14056  df-struct 16859  df-sets 16876  df-slot 16894  df-ndx 16906  df-base 16924  df-ress 16953  df-plusg 16986  df-mulr 16987  df-sca 16989  df-vsca 16990  df-ip 16991  df-tset 16992  df-ple 16993  df-ocomp 16994  df-ds 16995  df-hom 16997  df-cco 16998  df-0g 17163  df-gsum 17164  df-prds 17169  df-pws 17171  df-mre 17306  df-mrc 17307  df-mri 17308  df-acs 17309  df-proset 18024  df-drs 18025  df-poset 18042  df-ipo 18257  df-mgm 18337  df-sgrp 18386  df-mnd 18397  df-mhm 18441  df-submnd 18442  df-grp 18591  df-minusg 18592  df-sbg 18593  df-mulg 18712  df-subg 18763  df-ghm 18843  df-cntz 18934  df-cmn 19399  df-abl 19400  df-mgp 19732  df-ur 19749  df-ring 19796  df-oppr 19873  df-dvdsr 19894  df-unit 19895  df-invr 19925  df-drng 20004  df-subrg 20033  df-lmod 20136  df-lss 20205  df-lsp 20245  df-lmhm 20295  df-lbs 20348  df-lvec 20376  df-sra 20445  df-rgmod 20446  df-nzr 20540  df-dsmm 20950  df-frlm 20965  df-uvc 21001  df-lindf 21024  df-linds 21025  df-dim 31694
This theorem is referenced by:  extdgmul  31745
  Copyright terms: Public domain W3C validator