Step | Hyp | Ref
| Expression |
1 | | fedgmul.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ DivRing) |
2 | | fedgmul.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ DivRing) |
3 | | fedgmul.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) |
4 | | fedgmul.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹)) |
5 | | fedgmul.f |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝐸 ↾s 𝑈) |
6 | 5 | subsubrg 19251 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))) |
7 | 6 | biimpa 477 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)) |
8 | 3, 4, 7 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)) |
9 | 8 | simpld 495 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸)) |
10 | | fedgmul.a |
. . . . . . . . . . . 12
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉) |
11 | | fedgmul.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (𝐸 ↾s 𝑉) |
12 | 10, 11 | sralvec 30594 |
. . . . . . . . . . 11
⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) |
13 | 1, 2, 9, 12 | syl3anc 1364 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ LVec) |
14 | | lveclmod 19568 |
. . . . . . . . . 10
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ LMod) |
16 | | fedgmullem.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶)) |
17 | | eqid 2795 |
. . . . . . . . . . . 12
⊢
(Base‘𝐶) =
(Base‘𝐶) |
18 | | eqid 2795 |
. . . . . . . . . . . 12
⊢
(LBasis‘𝐶) =
(LBasis‘𝐶) |
19 | 17, 18 | lbsss 19539 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶)) |
20 | 16, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶)) |
21 | | eqid 2795 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐸) =
(Base‘𝐸) |
22 | 21 | subrgss 19226 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸)) |
23 | 3, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸)) |
24 | 5, 21 | ressbas2 16384 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 = (Base‘𝐹)) |
26 | | fedgmul.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉) |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉)) |
28 | | eqid 2795 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐹) =
(Base‘𝐹) |
29 | 28 | subrgss 19226 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹)) |
30 | 4, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹)) |
31 | 27, 30 | srabase 19640 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶)) |
32 | 25, 31 | eqtrd 2831 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 = (Base‘𝐶)) |
33 | 32, 23 | eqsstrrd 3927 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸)) |
34 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉)) |
35 | 21 | subrgss 19226 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸)) |
36 | 9, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸)) |
37 | 34, 36 | srabase 19640 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴)) |
38 | 33, 37 | sseqtrd 3928 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴)) |
39 | 20, 38 | sstrd 3899 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴)) |
40 | 34, 3, 36 | srasubrg 30593 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴)) |
41 | | subrgsubg 19231 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴)) |
43 | 10, 1, 9 | drgextvsca 30597 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (.r‘𝐸) = (
·𝑠 ‘𝐴)) |
44 | 43 | oveqdr 7044 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝐸)𝑦) = (𝑥( ·𝑠
‘𝐴)𝑦)) |
45 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ (SubRing‘𝐸)) |
46 | 8 | simprd 496 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉 ⊆ 𝑈) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 ⊆ 𝑈) |
48 | | simprl 767 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴))) |
49 | | ressabs 16392 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉)) |
50 | 3, 46, 49 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉)) |
51 | 5 | oveq1i 7026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉) |
52 | 50, 51, 11 | 3eqtr4g 2856 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾) |
53 | 27, 30 | srasca 19643 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶)) |
54 | 52, 53 | eqtr3d 2833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 = (Scalar‘𝐶)) |
55 | 54 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(Scalar‘𝐶))) |
56 | 11, 21 | ressbas2 16384 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾)) |
57 | 36, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑉 = (Base‘𝐾)) |
58 | 34, 36 | srasca 19643 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴)) |
59 | 11, 58 | syl5eq 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 = (Scalar‘𝐴)) |
60 | 59, 54 | eqtr3d 2833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶)) |
61 | 60 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶))) |
62 | 55, 57, 61 | 3eqtr4d 2841 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴))) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴))) |
64 | 48, 63 | eleqtrrd 2886 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉) |
65 | 47, 64 | sseldd 3890 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈) |
66 | | simprr 769 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
67 | | eqid 2795 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝐸) = (.r‘𝐸) |
68 | 67 | subrgmcl 19237 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈) |
69 | 45, 65, 66, 68 | syl3anc 1364 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈) |
70 | 44, 69 | eqeltrrd 2884 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈) |
71 | 70 | ralrimivva 3158 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈) |
72 | | eqid 2795 |
. . . . . . . . . . . . 13
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
73 | | eqid 2795 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴)) |
74 | | eqid 2795 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐴) =
(Base‘𝐴) |
75 | | eqid 2795 |
. . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
76 | | eqid 2795 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘𝐴) =
(LSubSp‘𝐴) |
77 | 72, 73, 74, 75, 76 | islss4 19424 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈))) |
78 | 77 | biimpar 478 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈
(Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴)) |
79 | 15, 42, 71, 78 | syl12anc 833 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴)) |
80 | 20, 32 | sseqtr4d 3929 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ 𝑈) |
81 | 18 | lbslinds 20659 |
. . . . . . . . . . . 12
⊢
(LBasis‘𝐶)
⊆ (LIndS‘𝐶) |
82 | 81, 16 | sseldi 3887 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶)) |
83 | 23, 37 | sseqtrd 3928 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴)) |
84 | | eqid 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ↾s 𝑈) = (𝐴 ↾s 𝑈) |
85 | 84, 74 | ressbas2 16384 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾s 𝑈))) |
86 | 83, 85 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾s 𝑈))) |
87 | 32, 86 | eqtr3d 2833 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾s 𝑈))) |
88 | 84, 72 | resssca 16479 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈))) |
89 | 3, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈))) |
90 | 60, 89 | eqtr3d 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾s 𝑈))) |
91 | 90 | fveq2d 6542 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾s 𝑈)))) |
92 | 90 | fveq2d 6542 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(0g‘(Scalar‘𝐶)) =
(0g‘(Scalar‘(𝐴 ↾s 𝑈)))) |
93 | | eqid 2795 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝐸) = (+g‘𝐸) |
94 | 5, 93 | ressplusg 16441 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(+g‘𝐸) =
(+g‘𝐹)) |
95 | 3, 94 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐹)) |
96 | 34, 36 | sraaddg 19641 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐴)) |
97 | 27, 30 | sraaddg 19641 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (+g‘𝐹) = (+g‘𝐶)) |
98 | 95, 96, 97 | 3eqtr3rd 2840 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (+g‘𝐶) = (+g‘𝐴)) |
99 | | eqid 2795 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝐴) = (+g‘𝐴) |
100 | 84, 99 | ressplusg 16441 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(+g‘𝐴) =
(+g‘(𝐴
↾s 𝑈))) |
101 | 3, 100 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (+g‘𝐴) = (+g‘(𝐴 ↾s 𝑈))) |
102 | 98, 101 | eqtrd 2831 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (+g‘𝐶) = (+g‘(𝐴 ↾s 𝑈))) |
103 | 102 | oveqdr 7044 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g‘𝐶)𝑦) = (𝑥(+g‘(𝐴 ↾s 𝑈))𝑦)) |
104 | | fedgmul.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ DivRing) |
105 | 52, 2 | eqeltrd 2883 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing) |
106 | | eqid 2795 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉) |
107 | 26, 106 | sralvec 30594 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec) |
108 | 104, 105,
4, 107 | syl3anc 1364 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ LVec) |
109 | | lveclmod 19568 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ LMod) |
111 | | eqid 2795 |
. . . . . . . . . . . . . . 15
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
112 | | eqid 2795 |
. . . . . . . . . . . . . . 15
⊢ (
·𝑠 ‘𝐶) = ( ·𝑠
‘𝐶) |
113 | | eqid 2795 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
114 | 17, 111, 112, 113 | lmodvscl 19341 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠
‘𝐶)𝑦) ∈ (Base‘𝐶)) |
115 | 114 | 3expb 1113 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠
‘𝐶)𝑦) ∈ (Base‘𝐶)) |
116 | 110, 115 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠
‘𝐶)𝑦) ∈ (Base‘𝐶)) |
117 | | fedgmul.b |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) |
118 | 117, 1, 3 | drgextvsca 30597 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (.r‘𝐸) = (
·𝑠 ‘𝐵)) |
119 | 43, 118 | eqtr3d 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐵)) |
120 | 5, 67 | ressmulr 16454 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(.r‘𝐸) =
(.r‘𝐹)) |
121 | 3, 120 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹)) |
122 | 26, 104, 4 | drgextvsca 30597 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (.r‘𝐹) = (
·𝑠 ‘𝐶)) |
123 | 121, 118,
122 | 3eqtr3d 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (
·𝑠 ‘𝐵) = ( ·𝑠
‘𝐶)) |
124 | 119, 123 | eqtr2d 2832 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (
·𝑠 ‘𝐶) = ( ·𝑠
‘𝐴)) |
125 | 84, 75 | ressvsca 16480 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘(𝐴
↾s 𝑈))) |
126 | 3, 125 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (
·𝑠 ‘𝐴) = ( ·𝑠
‘(𝐴
↾s 𝑈))) |
127 | 124, 126 | eqtrd 2831 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (
·𝑠 ‘𝐶) = ( ·𝑠
‘(𝐴
↾s 𝑈))) |
128 | 127 | oveqdr 7044 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠
‘𝐶)𝑦) = (𝑥( ·𝑠
‘(𝐴
↾s 𝑈))𝑦)) |
129 | | ovexd 7050 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ↾s 𝑈) ∈ V) |
130 | 87, 91, 92, 103, 116, 128, 108, 129 | lindspropd 30589 |
. . . . . . . . . . 11
⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾s 𝑈))) |
131 | 82, 130 | eleqtrd 2885 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈))) |
132 | 76, 84 | lsslinds 20657 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴))) |
133 | 132 | biimpa 477 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴)) |
134 | 15, 79, 80, 131, 133 | syl31anc 1366 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴)) |
135 | | eqid 2795 |
. . . . . . . . . . 11
⊢
(0g‘𝐴) = (0g‘𝐴) |
136 | | eqid 2795 |
. . . . . . . . . . 11
⊢
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐴)) |
137 | 74, 73, 72, 75, 135, 136 | islinds5 30580 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))})))) |
138 | 137 | biimpa 477 |
. . . . . . . . 9
⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
139 | 15, 39, 134, 138 | syl21anc 834 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
140 | 139 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
141 | | eqid 2795 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) |
142 | | fvexd 6553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) ∈ V) |
143 | | fedgmullem.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵)) |
144 | 143 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ∈ (LBasis‘𝐵)) |
145 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶)) |
146 | | fedgmullem2.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))) |
147 | | fvexd 6553 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Scalar‘𝐴) ∈ V) |
148 | 143, 16 | xpexd 7331 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 × 𝑋) ∈ V) |
149 | | eqid 2795 |
. . . . . . . . . . . . . . . . 17
⊢
((Scalar‘𝐴)
freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) |
150 | | eqid 2795 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) |
151 | 149, 73, 136, 150 | frlmelbas 20582 |
. . . . . . . . . . . . . . . 16
⊢
(((Scalar‘𝐴)
∈ V ∧ (𝑌 ×
𝑋) ∈ V) → (𝑊 ∈
(Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
(𝑌 × 𝑋)) ∧ 𝑊 finSupp
(0g‘(Scalar‘𝐴))))) |
152 | 147, 148,
151 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
(𝑌 × 𝑋)) ∧ 𝑊 finSupp
(0g‘(Scalar‘𝐴))))) |
153 | 146, 152 | mpbid 233 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
(𝑌 × 𝑋)) ∧ 𝑊 finSupp
(0g‘(Scalar‘𝐴)))) |
154 | 153 | simpld 495 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
(𝑌 × 𝑋))) |
155 | | fvexd 6553 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) ∈ V) |
156 | 155, 148 | elmapd 8270 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
(𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))) |
157 | 154, 156 | mpbid 233 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))) |
158 | 157 | ffnd 6383 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋)) |
159 | 158 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋)) |
160 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌) |
161 | 153 | simprd 496 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 finSupp
(0g‘(Scalar‘𝐴))) |
162 | | drngring 19199 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring) |
163 | 1, 162 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ∈ Ring) |
164 | | ringmnd 18996 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ Mnd) |
166 | | subrgsubg 19231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸)) |
167 | 9, 166 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸)) |
168 | | eqid 2795 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝐸) = (0g‘𝐸) |
169 | 168 | subg0cl 18041 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ (SubGrp‘𝐸) →
(0g‘𝐸)
∈ 𝑉) |
170 | 167, 169 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0g‘𝐸) ∈ 𝑉) |
171 | 46, 170 | sseldd 3890 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐸) ∈ 𝑈) |
172 | 5, 21, 168 | ress0g 17758 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 ∈ Mnd ∧
(0g‘𝐸)
∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) →
(0g‘𝐸) =
(0g‘𝐹)) |
173 | 165, 171,
23, 172 | syl3anc 1364 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐹)) |
174 | 54 | fveq2d 6542 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐾) =
(0g‘(Scalar‘𝐶))) |
175 | 11, 168 | subrg0 19232 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ (SubRing‘𝐸) →
(0g‘𝐸) =
(0g‘𝐾)) |
176 | 9, 175 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐾)) |
177 | 60 | fveq2d 6542 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐶))) |
178 | 174, 176,
177 | 3eqtr4d 2841 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝐸) =
(0g‘(Scalar‘𝐴))) |
179 | 173, 178 | eqtr3d 2833 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝐹) =
(0g‘(Scalar‘𝐴))) |
180 | 161, 179 | breqtrrd 4990 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 finSupp (0g‘𝐹)) |
181 | 180 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0g‘𝐹)) |
182 | 141, 142,
144, 145, 159, 160, 181 | fsuppcurry1 30149 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘𝐹)) |
183 | 179 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) =
(0g‘(Scalar‘𝐴))) |
184 | 182, 183 | breqtrd 4988 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴))) |
185 | | eqidd 2796 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
186 | 157 | fovrnda 7175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴))) |
187 | 186 | anassrs 468 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴))) |
188 | 185, 187 | fvmpt2d 6647 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖)) |
189 | 188 | oveq1d 7031 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)) |
190 | 119 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐵)) |
191 | 190 | oveqd 7033 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) |
192 | 189, 191 | eqtrd 2831 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) |
193 | 192 | mpteq2dva 5055 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) |
194 | 193 | oveq2d 7032 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
195 | 1 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ DivRing) |
196 | 9 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ∈ (SubRing‘𝐸)) |
197 | 2 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐾 ∈ DivRing) |
198 | 10, 195, 196, 11, 197, 145 | drgextgsum 30601 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
199 | 3 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸)) |
200 | 104 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing) |
201 | 117, 195,
199, 5, 200, 145 | drgextgsum 30601 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
202 | 198, 201 | eqtr3d 2833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
203 | 194, 202 | eqtrd 2831 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
204 | 143 | mptexd 6853 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ V) |
205 | | eqid 2795 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘𝐵) = (0g‘𝐵) |
206 | 117, 5 | sralvec 30594 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec) |
207 | 1, 104, 3, 206 | syl3anc 1364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ∈ LVec) |
208 | | lveclmod 19568 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod) |
209 | 207, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵 ∈ LMod) |
210 | 209 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod) |
211 | | lmodabl 19371 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel) |
213 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈)) |
214 | 213, 3, 23 | srasubrg 30593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵)) |
215 | | subrgsubg 19231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵)) |
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵)) |
217 | 216 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵)) |
218 | 110 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod) |
219 | 61 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) =
(Base‘(Scalar‘𝐶))) |
220 | 187, 219 | eleqtrd 2885 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶))) |
221 | 20 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶)) |
222 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
223 | 221, 222 | sseldd 3890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶)) |
224 | 17, 111, 112, 113 | lmodvscl 19341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖) ∈ (Base‘𝐶)) |
225 | 218, 220,
223, 224 | syl3anc 1364 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖) ∈ (Base‘𝐶)) |
226 | 123 | oveqd 7033 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖)) |
227 | 226 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖)) |
228 | 32 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶)) |
229 | 225, 227,
228 | 3eltr4d 2898 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) ∈ 𝑈) |
230 | 229 | fmpttd 6742 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)):𝑋⟶𝑈) |
231 | 213, 23 | srasca 19643 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵)) |
232 | 5, 231 | syl5eq 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 = (Scalar‘𝐵)) |
233 | 232 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵)) |
234 | | eqid 2795 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝐵) =
(Base‘𝐵) |
235 | | ovexd 7050 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V) |
236 | 20, 33 | sstrd 3899 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸)) |
237 | 236 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸)) |
238 | | simprr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋) |
239 | 237, 238 | sseldd 3890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸)) |
240 | 239 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸)) |
241 | 213, 23 | srabase 19640 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵)) |
242 | 241 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵)) |
243 | 240, 242 | eleqtrd 2885 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵)) |
244 | | eqid 2795 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝐹) = (0g‘𝐹) |
245 | | eqid 2795 |
. . . . . . . . . . . . . . . . . . 19
⊢ (
·𝑠 ‘𝐵) = ( ·𝑠
‘𝐵) |
246 | 145, 210,
233, 234, 235, 243, 205, 244, 245, 182 | mptscmfsupp0 19389 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) finSupp (0g‘𝐵)) |
247 | 205, 212,
145, 217, 230, 246 | gsumsubgcl 18760 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ 𝑈) |
248 | 232 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (Base‘𝐹) =
(Base‘(Scalar‘𝐵))) |
249 | 25, 248 | eqtrd 2831 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵))) |
250 | 249 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵))) |
251 | 247, 250 | eleqtrd 2885 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵))) |
252 | 251 | fmpttd 6742 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) |
253 | 252 | ffund 6386 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))) |
254 | | fvexd 6553 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(0g‘(Scalar‘𝐵)) ∈ V) |
255 | | fconstmpt 5500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) |
256 | 255 | eqeq2i 2807 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
257 | | ovex 7048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘𝑊𝑖) ∈ V |
258 | 257 | rgenw 3117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∀𝑖 ∈
𝑋 (𝑘𝑊𝑖) ∈ V |
259 | | mpteqb 6653 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑖 ∈
𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
260 | 258, 259 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
261 | 256, 260 | bitri 276 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
262 | 261 | necon3abii 3030 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
263 | | df-ov 7019 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘𝑊𝑖) = (𝑊‘〈𝑘, 𝑖〉) |
264 | 263 | eqcomi 2804 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊‘〈𝑘, 𝑖〉) = (𝑘𝑊𝑖) |
265 | 264 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘〈𝑘, 𝑖〉) = (𝑘𝑊𝑖)) |
266 | 265 | eqeq1d 2797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘〈𝑘, 𝑖〉) =
(0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
267 | 266 | necon3abid 3020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
268 | 267 | rexbidva 3259 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
269 | | rexnal 3202 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑖 ∈
𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
270 | 268, 269 | syl6rbb 289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)))) |
271 | 262, 270 | syl5bb 284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)))) |
272 | 271 | rabbidva 3424 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴))}) |
273 | | fveq2 6538 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑘, 𝑖〉 → (𝑊‘𝑧) = (𝑊‘〈𝑘, 𝑖〉)) |
274 | 273 | neeq1d 3043 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑘, 𝑖〉 → ((𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴)) ↔ (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)))) |
275 | 274 | dmrab 29952 |
. . . . . . . . . . . . . . . 16
⊢ dom
{𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴))} |
276 | 272, 275 | syl6eqr 2849 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))}) |
277 | | fvexd 6553 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(0g‘(Scalar‘𝐴)) ∈ V) |
278 | | suppvalfn 7688 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧
(0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp
(0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))}) |
279 | 158, 148,
277, 278 | syl3anc 1364 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑊 supp
(0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))}) |
280 | 161 | fsuppimpd 8686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑊 supp
(0g‘(Scalar‘𝐴))) ∈ Fin) |
281 | 279, 280 | eqeltrrd 2884 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin) |
282 | | dmfi 8648 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin) |
283 | 281, 282 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin) |
284 | 276, 283 | eqeltrd 2883 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} ∈ Fin) |
285 | | nfv 1892 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖𝜑 |
286 | | nfcv 2949 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑖𝑌 |
287 | | nfmpt1 5058 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) |
288 | | nfcv 2949 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑖(𝑋 ×
{(0g‘(Scalar‘𝐴))}) |
289 | 287, 288 | nfne 3087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) |
290 | 289, 286 | nfrab 3345 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} |
291 | 286, 290 | nfdif 4023 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
292 | 291 | nfcriv 2939 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
293 | 285, 292 | nfan 1881 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) |
294 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) |
295 | 294 | eldifad 3871 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌) |
296 | 294 | eldifbd 3872 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
297 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖)) |
298 | 297 | mpteq2dv 5056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
299 | 298 | neeq1d 3043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
300 | 299 | elrab 3618 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
301 | 296, 300 | sylnib 329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
302 | 295, 301 | mpnanrd 410 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
303 | | nne 2988 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
304 | 302, 303 | sylib 219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
305 | 304, 255 | syl6eq 2847 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
306 | | ovex 7048 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗𝑊𝑖) ∈ V |
307 | 306 | rgenw 3117 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
∀𝑖 ∈
𝑋 (𝑗𝑊𝑖) ∈ V |
308 | | mpteqb 6653 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑖 ∈
𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
309 | 307, 308 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
310 | 305, 309 | sylib 219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
311 | 310 | r19.21bi 3175 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
312 | 311 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = ((0g‘(Scalar‘𝐴))(
·𝑠 ‘𝐵)𝑖)) |
313 | 117, 1, 3 | drgext0g 30596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) |
314 | 117, 1, 3 | drgext0gsca 30598 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0g‘𝐵) =
(0g‘(Scalar‘𝐵))) |
315 | 313, 178,
314 | 3eqtr3d 2839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐵))) |
316 | 315 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐵))) |
317 | 316 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) →
((0g‘(Scalar‘𝐴))( ·𝑠
‘𝐵)𝑖) = ((0g‘(Scalar‘𝐵))(
·𝑠 ‘𝐵)𝑖)) |
318 | 209 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod) |
319 | 295, 243 | syldanl 601 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵)) |
320 | | eqid 2795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Scalar‘𝐵) =
(Scalar‘𝐵) |
321 | | eqid 2795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘(Scalar‘𝐵)) =
(0g‘(Scalar‘𝐵)) |
322 | 234, 320,
245, 321, 205 | lmod0vs 19357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) →
((0g‘(Scalar‘𝐵))( ·𝑠
‘𝐵)𝑖) = (0g‘𝐵)) |
323 | 318, 319,
322 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) →
((0g‘(Scalar‘𝐵))( ·𝑠
‘𝐵)𝑖) = (0g‘𝐵)) |
324 | 312, 317,
323 | 3eqtrd 2835 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = (0g‘𝐵)) |
325 | 293, 324 | mpteq2da 5054 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) |
326 | 325 | oveq2d 7032 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵)))) |
327 | 209, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ Abel) |
328 | | ablgrp 18638 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp) |
329 | | grpmnd 17868 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd) |
330 | 327, 328,
329 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈ Mnd) |
331 | 205 | gsumz 17813 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵)) |
332 | 330, 16, 331 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵)) |
333 | 332 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵)) |
334 | 314 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (0g‘𝐵) =
(0g‘(Scalar‘𝐵))) |
335 | 326, 333,
334 | 3eqtrd 2835 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
336 | 335, 143 | suppss2 7715 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) supp
(0g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
337 | | suppssfifsupp 8694 |
. . . . . . . . . . . . . 14
⊢ ((((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ V ∧ Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∧
(0g‘(Scalar‘𝐵)) ∈ V) ∧ ({𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} ∈ Fin ∧ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) supp
(0g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵))) |
338 | 204, 253,
254, 284, 336, 337 | syl32anc 1371 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵))) |
339 | | eqidd 2796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))) |
340 | | ovexd 7050 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V) |
341 | 339, 340 | fvmpt2d 6647 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
342 | 341 | oveq1d 7031 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
343 | 342 | mpteq2dva 5055 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) |
344 | 343 | oveq2d 7032 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
345 | 119 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐵)) |
346 | 43 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (.r‘𝐸) = (
·𝑠 ‘𝐴)) |
347 | 346 | oveqd 7033 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)) |
348 | 347 | mpteq2dva 5055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖))) |
349 | 118 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = (
·𝑠 ‘𝐵)) |
350 | 349 | oveqd 7033 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) |
351 | 350 | mpteq2dv 5056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) |
352 | 348, 351 | eqtr3d 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) |
353 | 352 | oveq2d 7032 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
354 | | eqidd 2796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗) |
355 | 345, 353,
354 | oveq123d 7037 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
356 | 202 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
357 | 355, 356 | eqtrd 2831 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
358 | 357 | mpteq2dva 5055 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) |
359 | 358 | oveq2d 7032 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
360 | 10, 21 | sraring 30591 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring) |
361 | 163, 36, 360 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ Ring) |
362 | | ringcmn 19021 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd) |
363 | 361, 362 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ CMnd) |
364 | 163 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring) |
365 | | eqid 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(LBasis‘𝐵) =
(LBasis‘𝐵) |
366 | 234, 365 | lbsss 19539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵)) |
367 | 143, 366 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵)) |
368 | 367, 241 | sseqtr4d 3929 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸)) |
369 | 368 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸)) |
370 | | simprl 767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌) |
371 | 369, 370 | sseldd 3890 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸)) |
372 | 21, 67 | ringcl 19001 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸)) |
373 | 364, 239,
371, 372 | syl3anc 1364 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸)) |
374 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴)) |
375 | 373, 374 | eleqtrd 2885 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴)) |
376 | 375 | ralrimivva 3158 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴)) |
377 | | fedgmullem.d |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗)) |
378 | 377 | fmpo 7622 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑗 ∈
𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴)) |
379 | 376, 378 | sylib 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴)) |
380 | 72, 73, 75, 74, 15, 157, 379, 148 | lcomf 19363 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴)) |
381 | 72, 73, 75, 74, 15, 157, 379, 148, 135, 136, 161 | lcomfsupp 19364 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷) finSupp (0g‘𝐴)) |
382 | 74, 135, 363, 143, 16, 380, 381 | gsumxp 18816 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 Σg (𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖)))))) |
383 | | fedgmullem2.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 Σg (𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)) = (0g‘𝐴)) |
384 | 163 | 3ad2ant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring) |
385 | 157 | 3ad2ant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))) |
386 | 57, 55 | eqtrd 2831 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶))) |
387 | 386, 36 | eqsstrrd 3927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 →
(Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸)) |
388 | 61, 387 | eqsstrd 3926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸)) |
389 | 388, 37 | sseqtrd 3928 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴)) |
390 | 389 | 3ad2ant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴)) |
391 | 385, 390 | fssd 6396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴)) |
392 | | simp2 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌) |
393 | | simp3 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
394 | 391, 392,
393 | fovrnd 7176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴)) |
395 | 37 | 3ad2ant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴)) |
396 | 394, 395 | eleqtrrd 2886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸)) |
397 | 239 | 3impb 1108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸)) |
398 | 371 | 3impb 1108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸)) |
399 | 21, 67 | ringass 19004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) |
400 | 384, 396,
397, 398, 399 | syl13anc 1365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) |
401 | 400 | mpoeq3dva 7089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) |
402 | | ovexd 7050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V) |
403 | | ovexd 7050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ V) |
404 | | fnov 7138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
405 | 158, 404 | sylib 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
406 | 377 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗))) |
407 | 143, 16, 402, 403, 405, 406 | offval22 7639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑊 ∘𝑓
(.r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) |
408 | | ofeq 7269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((.r‘𝐸) = ( ·𝑠
‘𝐴) →
∘𝑓 (.r‘𝐸) = ∘𝑓 (
·𝑠 ‘𝐴)) |
409 | 43, 408 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 →
∘𝑓 (.r‘𝐸) = ∘𝑓 (
·𝑠 ‘𝐴)) |
410 | 409 | oveqd 7033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑊 ∘𝑓
(.r‘𝐸)𝐷) = (𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)) |
411 | 401, 407,
410 | 3eqtr2rd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) |
412 | 411 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) |
413 | 412 | oveqd 7033 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖)) |
414 | | simplr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌) |
415 | | ovexd 7050 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V) |
416 | | eqid 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
417 | 416 | ovmpt4g 7153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
418 | 414, 222,
415, 417 | syl3anc 1364 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
419 | 413, 418 | eqtrd 2831 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
420 | 419 | mpteq2dva 5055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) |
421 | 420 | oveq2d 7032 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))) |
422 | 163 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring) |
423 | 368 | sselda 3889 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸)) |
424 | 163 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring) |
425 | 387 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸)) |
426 | 425, 220 | sseldd 3890 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸)) |
427 | 21, 67 | ringcl 19001 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸)) |
428 | 424, 426,
240, 427 | syl3anc 1364 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸)) |
429 | 313 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐸) = (0g‘𝐵)) |
430 | 246, 351,
429 | 3brtr4d 4994 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) finSupp (0g‘𝐸)) |
431 | 21, 168, 93, 67, 422, 145, 423, 428, 430 | gsummulc1 19046 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗)) |
432 | 421, 431 | eqtrd 2831 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗)) |
433 | 145 | mptexd 6853 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖)) ∈ V) |
434 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod) |
435 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸)) |
436 | 10, 433, 195, 434, 435 | gsumsra 30493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖)))) |
437 | 145 | mptexd 6853 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) ∈ V) |
438 | 10, 437, 195, 434, 435 | gsumsra 30493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))) |
439 | 438 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗)) |
440 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = (
·𝑠 ‘𝐴)) |
441 | 348 | oveq2d 7032 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))) |
442 | 440, 441,
354 | oveq123d 7037 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) |
443 | 439, 442 | eqtrd 2831 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) |
444 | 432, 436,
443 | 3eqtr3d 2839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) |
445 | 444 | mpteq2dva 5055 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) |
446 | 445 | oveq2d 7032 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘𝑓 (
·𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)))) |
447 | 382, 383,
446 | 3eqtr3rd 2840 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) = (0g‘𝐴)) |
448 | 10, 1, 9 | drgext0g 30596 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐴)) |
449 | 447, 448,
313 | 3eqtr2d 2837 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) = (0g‘𝐵)) |
450 | 10, 1, 9, 11, 2, 143 | drgextgsum 30601 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
451 | 117, 1, 3, 5, 104, 143 | drgextgsum 30601 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
452 | 450, 451 | eqtr3d 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
453 | 359, 449,
452 | 3eqtr3rd 2840 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) |
454 | 344, 453 | eqtrd 2831 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) |
455 | | breq1 4965 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑏 finSupp
(0g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)))) |
456 | | nfmpt1 5058 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
457 | 456 | nfeq2 2964 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
458 | | fveq1 6537 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)) |
459 | 458 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)) |
460 | 459 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)) |
461 | 457, 460 | mpteq2da 5054 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) |
462 | 461 | oveq2d 7032 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)))) |
463 | 462 | eqeq1d 2797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → ((𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵) ↔ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵))) |
464 | 455, 463 | anbi12d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → ((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)))) |
465 | | eqeq1 2799 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
466 | 464, 465 | imbi12d 346 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))})) ↔ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))})))) |
467 | 365 | lbslinds 20659 |
. . . . . . . . . . . . . . . 16
⊢
(LBasis‘𝐵)
⊆ (LIndS‘𝐵) |
468 | 467, 143 | sseldi 3887 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵)) |
469 | | eqid 2795 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵)) |
470 | 234, 469,
320, 245, 205, 321 | islinds5 30580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑𝑚
𝑌)((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))})))) |
471 | 470 | biimpa 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑𝑚
𝑌)((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
472 | 209, 367,
468, 471 | syl21anc 834 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑𝑚
𝑌)((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
473 | | fvexd 6553 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Base‘(Scalar‘𝐵)) ∈ V) |
474 | | elmapg 8269 |
. . . . . . . . . . . . . . . 16
⊢
(((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑𝑚
𝑌) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))) |
475 | 474 | biimpar 478 |
. . . . . . . . . . . . . . 15
⊢
((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑𝑚
𝑌)) |
476 | 473, 143,
252, 475 | syl21anc 834 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑𝑚
𝑌)) |
477 | 466, 472,
476 | rspcdva 3565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
478 | 338, 454,
477 | mp2and 695 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))})) |
479 | | fconstmpt 5500 |
. . . . . . . . . . . 12
⊢ (𝑌 ×
{(0g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵))) |
480 | 478, 479 | syl6eq 2847 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵)))) |
481 | | ovex 7048 |
. . . . . . . . . . . . 13
⊢ (𝐵 Σg
(𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V |
482 | 481 | rgenw 3117 |
. . . . . . . . . . . 12
⊢
∀𝑗 ∈
𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V |
483 | | mpteqb 6653 |
. . . . . . . . . . . 12
⊢
(∀𝑗 ∈
𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵)))) |
484 | 482, 483 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
485 | 480, 484 | sylib 219 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
486 | 485 | r19.21bi 3175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
487 | 313, 448,
314 | 3eqtr3rd 2840 |
. . . . . . . . . 10
⊢ (𝜑 →
(0g‘(Scalar‘𝐵)) = (0g‘𝐴)) |
488 | 487 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) →
(0g‘(Scalar‘𝐵)) = (0g‘𝐴)) |
489 | 203, 486,
488 | 3eqtrd 2835 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) |
490 | 184, 489 | jca 512 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴))) |
491 | 187 | fmpttd 6742 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))) |
492 | | fvexd 6553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V) |
493 | 492, 145 | elmapd 8270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))) |
494 | 491, 493 | mpbird 258 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
𝑋)) |
495 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
496 | 495 | breq1d 4972 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp
(0g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)))) |
497 | | nfv 1892 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌) |
498 | | nfmpt1 5058 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) |
499 | 498 | nfeq2 2964 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) |
500 | 497, 499 | nfan 1881 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
501 | | simplr 765 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
502 | 501 | fveq1d 6540 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)) |
503 | 502 | oveq1d 7031 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖)) |
504 | 500, 503 | mpteq2da 5054 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) |
505 | 504 | oveq2d 7032 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖)))) |
506 | 505 | eqeq1d 2797 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴) ↔ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴))) |
507 | 496, 506 | anbi12d 630 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)))) |
508 | 495 | eqeq1d 2797 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
509 | 507, 508 | imbi12d 346 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) ↔ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})))) |
510 | 494, 509 | rspcdv 3562 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑𝑚
𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})))) |
511 | 140, 490,
510 | mp2d 49 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
512 | 511, 255 | syl6eq 2847 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
513 | 512, 309 | sylib 219 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
514 | 513 | ralrimiva 3149 |
. . 3
⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
515 | | eqidd 2796 |
. . . 4
⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐴))) |
516 | | fvexd 6553 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) →
(0g‘(Scalar‘𝐴)) ∈ V) |
517 | | fvexd 6553 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) →
(0g‘(Scalar‘𝐴)) ∈ V) |
518 | 158, 515,
516, 517 | fnmpoovd 7638 |
. . 3
⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
519 | 514, 518 | mpbird 258 |
. 2
⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
520 | | fconstmpo 7125 |
. 2
⊢ ((𝑌 × 𝑋) ×
{(0g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) |
521 | 519, 520 | syl6eqr 2849 |
1
⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) ×
{(0g‘(Scalar‘𝐴))})) |