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