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 19554 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))) |
7 | 6 | biimpa 480 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)) |
8 | 3, 4, 7 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)) |
9 | 8 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸)) |
10 | | fedgmul.a |
. . . . . . . . . . . 12
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉) |
11 | | fedgmul.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (𝐸 ↾s 𝑉) |
12 | 10, 11 | sralvec 31078 |
. . . . . . . . . . 11
⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) |
13 | 1, 2, 9, 12 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ LVec) |
14 | | lveclmod 19871 |
. . . . . . . . . 10
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ LMod) |
16 | | fedgmullem.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶)) |
17 | | eqid 2798 |
. . . . . . . . . . . 12
⊢
(Base‘𝐶) =
(Base‘𝐶) |
18 | | eqid 2798 |
. . . . . . . . . . . 12
⊢
(LBasis‘𝐶) =
(LBasis‘𝐶) |
19 | 17, 18 | lbsss 19842 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶)) |
20 | 16, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶)) |
21 | | eqid 2798 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐸) =
(Base‘𝐸) |
22 | 21 | subrgss 19529 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸)) |
23 | 3, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸)) |
24 | 5, 21 | ressbas2 16547 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 = (Base‘𝐹)) |
26 | | fedgmul.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉) |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉)) |
28 | | eqid 2798 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐹) =
(Base‘𝐹) |
29 | 28 | subrgss 19529 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹)) |
30 | 4, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹)) |
31 | 27, 30 | srabase 19943 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶)) |
32 | 25, 31 | eqtrd 2833 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 = (Base‘𝐶)) |
33 | 32, 23 | eqsstrrd 3954 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸)) |
34 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉)) |
35 | 21 | subrgss 19529 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸)) |
36 | 9, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸)) |
37 | 34, 36 | srabase 19943 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴)) |
38 | 33, 37 | sseqtrd 3955 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴)) |
39 | 20, 38 | sstrd 3925 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴)) |
40 | 34, 3, 36 | srasubrg 31077 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴)) |
41 | | subrgsubg 19534 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴)) |
43 | 10, 1, 9 | drgextvsca 31081 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (.r‘𝐸) = (
·𝑠 ‘𝐴)) |
44 | 43 | oveqdr 7163 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝐸)𝑦) = (𝑥( ·𝑠
‘𝐴)𝑦)) |
45 | 3 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ (SubRing‘𝐸)) |
46 | 8 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉 ⊆ 𝑈) |
47 | 46 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 ⊆ 𝑈) |
48 | | simprl 770 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴))) |
49 | | ressabs 16555 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉)) |
50 | 3, 46, 49 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉)) |
51 | 5 | oveq1i 7145 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉) |
52 | 50, 51, 11 | 3eqtr4g 2858 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾) |
53 | 27, 30 | srasca 19946 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶)) |
54 | 52, 53 | eqtr3d 2835 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 = (Scalar‘𝐶)) |
55 | 54 | fveq2d 6649 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(Scalar‘𝐶))) |
56 | 11, 21 | ressbas2 16547 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾)) |
57 | 36, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑉 = (Base‘𝐾)) |
58 | 34, 36 | srasca 19946 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴)) |
59 | 11, 58 | syl5eq 2845 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 = (Scalar‘𝐴)) |
60 | 52, 53, 59 | 3eqtr3rd 2842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶)) |
61 | 60 | fveq2d 6649 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶))) |
62 | 55, 57, 61 | 3eqtr4d 2843 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴))) |
63 | 62 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴))) |
64 | 48, 63 | eleqtrrd 2893 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉) |
65 | 47, 64 | sseldd 3916 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈) |
66 | | simprr 772 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
67 | | eqid 2798 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝐸) = (.r‘𝐸) |
68 | 67 | subrgmcl 19540 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈) |
69 | 45, 65, 66, 68 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈) |
70 | 44, 69 | eqeltrrd 2891 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈) |
71 | 70 | ralrimivva 3156 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈) |
72 | | eqid 2798 |
. . . . . . . . . . . . 13
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
73 | | eqid 2798 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴)) |
74 | | eqid 2798 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐴) =
(Base‘𝐴) |
75 | | eqid 2798 |
. . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
76 | | eqid 2798 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘𝐴) =
(LSubSp‘𝐴) |
77 | 72, 73, 74, 75, 76 | islss4 19727 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈))) |
78 | 77 | biimpar 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈
(Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠
‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴)) |
79 | 15, 42, 71, 78 | syl12anc 835 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴)) |
80 | 20, 32 | sseqtrrd 3956 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ 𝑈) |
81 | 18 | lbslinds 20522 |
. . . . . . . . . . . 12
⊢
(LBasis‘𝐶)
⊆ (LIndS‘𝐶) |
82 | 81, 16 | sseldi 3913 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶)) |
83 | 23, 37 | sseqtrd 3955 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴)) |
84 | | eqid 2798 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ↾s 𝑈) = (𝐴 ↾s 𝑈) |
85 | 84, 74 | ressbas2 16547 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾s 𝑈))) |
86 | 83, 85 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾s 𝑈))) |
87 | 25, 86, 31 | 3eqtr3rd 2842 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾s 𝑈))) |
88 | 84, 72 | resssca 16642 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈))) |
89 | 3, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈))) |
90 | 60, 89 | eqtr3d 2835 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾s 𝑈))) |
91 | 90 | fveq2d 6649 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾s 𝑈)))) |
92 | 90 | fveq2d 6649 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(0g‘(Scalar‘𝐶)) =
(0g‘(Scalar‘(𝐴 ↾s 𝑈)))) |
93 | | eqid 2798 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝐸) = (+g‘𝐸) |
94 | 5, 93 | ressplusg 16604 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(+g‘𝐸) =
(+g‘𝐹)) |
95 | 3, 94 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐹)) |
96 | 34, 36 | sraaddg 19944 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐴)) |
97 | 27, 30 | sraaddg 19944 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (+g‘𝐹) = (+g‘𝐶)) |
98 | 95, 96, 97 | 3eqtr3rd 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (+g‘𝐶) = (+g‘𝐴)) |
99 | | eqid 2798 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝐴) = (+g‘𝐴) |
100 | 84, 99 | ressplusg 16604 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(+g‘𝐴) =
(+g‘(𝐴
↾s 𝑈))) |
101 | 3, 100 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (+g‘𝐴) = (+g‘(𝐴 ↾s 𝑈))) |
102 | 98, 101 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (+g‘𝐶) = (+g‘(𝐴 ↾s 𝑈))) |
103 | 102 | oveqdr 7163 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g‘𝐶)𝑦) = (𝑥(+g‘(𝐴 ↾s 𝑈))𝑦)) |
104 | | fedgmul.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ DivRing) |
105 | 52, 2 | eqeltrd 2890 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing) |
106 | | eqid 2798 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉) |
107 | 26, 106 | sralvec 31078 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec) |
108 | 104, 105,
4, 107 | syl3anc 1368 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ LVec) |
109 | | lveclmod 19871 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ LMod) |
111 | | eqid 2798 |
. . . . . . . . . . . . . . 15
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
112 | | eqid 2798 |
. . . . . . . . . . . . . . 15
⊢ (
·𝑠 ‘𝐶) = ( ·𝑠
‘𝐶) |
113 | | eqid 2798 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
114 | 17, 111, 112, 113 | lmodvscl 19644 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠
‘𝐶)𝑦) ∈ (Base‘𝐶)) |
115 | 114 | 3expb 1117 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠
‘𝐶)𝑦) ∈ (Base‘𝐶)) |
116 | 110, 115 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠
‘𝐶)𝑦) ∈ (Base‘𝐶)) |
117 | | fedgmul.b |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) |
118 | 117, 1, 3 | drgextvsca 31081 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (.r‘𝐸) = (
·𝑠 ‘𝐵)) |
119 | 43, 118 | eqtr3d 2835 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐵)) |
120 | 84, 75 | ressvsca 16643 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubRing‘𝐸) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘(𝐴
↾s 𝑈))) |
121 | 3, 120 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (
·𝑠 ‘𝐴) = ( ·𝑠
‘(𝐴
↾s 𝑈))) |
122 | 5, 67 | ressmulr 16617 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(.r‘𝐸) =
(.r‘𝐹)) |
123 | 3, 122 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹)) |
124 | 26, 104, 4 | drgextvsca 31081 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (.r‘𝐹) = (
·𝑠 ‘𝐶)) |
125 | 123, 118,
124 | 3eqtr3d 2841 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (
·𝑠 ‘𝐵) = ( ·𝑠
‘𝐶)) |
126 | 119, 121,
125 | 3eqtr3rd 2842 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (
·𝑠 ‘𝐶) = ( ·𝑠
‘(𝐴
↾s 𝑈))) |
127 | 126 | oveqdr 7163 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠
‘𝐶)𝑦) = (𝑥( ·𝑠
‘(𝐴
↾s 𝑈))𝑦)) |
128 | | ovexd 7170 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ↾s 𝑈) ∈ V) |
129 | 87, 91, 92, 103, 116, 127, 108, 128 | lindspropd 30997 |
. . . . . . . . . . 11
⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾s 𝑈))) |
130 | 82, 129 | eleqtrd 2892 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈))) |
131 | 76, 84 | lsslinds 20520 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴))) |
132 | 131 | biimpa 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴)) |
133 | 15, 79, 80, 130, 132 | syl31anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴)) |
134 | | eqid 2798 |
. . . . . . . . . . 11
⊢
(0g‘𝐴) = (0g‘𝐴) |
135 | | eqid 2798 |
. . . . . . . . . . 11
⊢
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐴)) |
136 | 74, 73, 72, 75, 134, 135 | islinds5 30983 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))})))) |
137 | 136 | biimpa 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
138 | 15, 39, 133, 137 | syl21anc 836 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
139 | 138 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
140 | | eqid 2798 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) |
141 | | fvexd 6660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) ∈ V) |
142 | | fedgmullem.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵)) |
143 | 142 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ∈ (LBasis‘𝐵)) |
144 | 16 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶)) |
145 | | fedgmullem2.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))) |
146 | | fvexd 6660 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Scalar‘𝐴) ∈ V) |
147 | 142, 16 | xpexd 7454 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 × 𝑋) ∈ V) |
148 | | eqid 2798 |
. . . . . . . . . . . . . . . . 17
⊢
((Scalar‘𝐴)
freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) |
149 | | eqid 2798 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) |
150 | 148, 73, 135, 149 | frlmelbas 20445 |
. . . . . . . . . . . . . . . 16
⊢
(((Scalar‘𝐴)
∈ V ∧ (𝑌 ×
𝑋) ∈ V) → (𝑊 ∈
(Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp
(0g‘(Scalar‘𝐴))))) |
151 | 146, 147,
150 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp
(0g‘(Scalar‘𝐴))))) |
152 | 145, 151 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp
(0g‘(Scalar‘𝐴)))) |
153 | 152 | simpld 498 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋))) |
154 | | fvexd 6660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) ∈ V) |
155 | 154, 147 | elmapd 8403 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))) |
156 | 153, 155 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))) |
157 | 156 | ffnd 6488 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋)) |
158 | 157 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋)) |
159 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌) |
160 | 152 | simprd 499 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 finSupp
(0g‘(Scalar‘𝐴))) |
161 | | drngring 19502 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring) |
162 | 1, 161 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ∈ Ring) |
163 | | ringmnd 19300 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ Mnd) |
165 | | subrgsubg 19534 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸)) |
166 | 9, 165 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸)) |
167 | | eqid 2798 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝐸) = (0g‘𝐸) |
168 | 167 | subg0cl 18279 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ (SubGrp‘𝐸) →
(0g‘𝐸)
∈ 𝑉) |
169 | 166, 168 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0g‘𝐸) ∈ 𝑉) |
170 | 46, 169 | sseldd 3916 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐸) ∈ 𝑈) |
171 | 5, 21, 167 | ress0g 17931 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 ∈ Mnd ∧
(0g‘𝐸)
∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) →
(0g‘𝐸) =
(0g‘𝐹)) |
172 | 164, 170,
23, 171 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐹)) |
173 | 54 | fveq2d 6649 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐾) =
(0g‘(Scalar‘𝐶))) |
174 | 11, 167 | subrg0 19535 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ (SubRing‘𝐸) →
(0g‘𝐸) =
(0g‘𝐾)) |
175 | 9, 174 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐾)) |
176 | 60 | fveq2d 6649 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐶))) |
177 | 173, 175,
176 | 3eqtr4d 2843 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝐸) =
(0g‘(Scalar‘𝐴))) |
178 | 172, 177 | eqtr3d 2835 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝐹) =
(0g‘(Scalar‘𝐴))) |
179 | 160, 178 | breqtrrd 5058 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 finSupp (0g‘𝐹)) |
180 | 179 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0g‘𝐹)) |
181 | 140, 141,
143, 144, 158, 159, 180 | fsuppcurry1 30487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘𝐹)) |
182 | 178 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) =
(0g‘(Scalar‘𝐴))) |
183 | 181, 182 | breqtrd 5056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴))) |
184 | | eqidd 2799 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
185 | 156 | fovrnda 7299 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴))) |
186 | 185 | anassrs 471 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴))) |
187 | 184, 186 | fvmpt2d 6758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖)) |
188 | 187 | oveq1d 7150 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)) |
189 | 119 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐵)) |
190 | 189 | oveqd 7152 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) |
191 | 188, 190 | eqtrd 2833 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) |
192 | 191 | mpteq2dva 5125 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) |
193 | 192 | oveq2d 7151 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
194 | 1 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ DivRing) |
195 | 9 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ∈ (SubRing‘𝐸)) |
196 | 2 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐾 ∈ DivRing) |
197 | 10, 194, 195, 11, 196, 144 | drgextgsum 31085 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
198 | 3 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸)) |
199 | 104 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing) |
200 | 117, 194,
198, 5, 199, 144 | drgextgsum 31085 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
201 | 197, 200 | eqtr3d 2835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
202 | 193, 201 | eqtrd 2833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
203 | 142 | mptexd 6964 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ V) |
204 | | eqid 2798 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘𝐵) = (0g‘𝐵) |
205 | 117, 5 | sralvec 31078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec) |
206 | 1, 104, 3, 205 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ∈ LVec) |
207 | | lveclmod 19871 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod) |
208 | 206, 207 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵 ∈ LMod) |
209 | 208 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod) |
210 | | lmodabl 19674 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel) |
211 | 209, 210 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel) |
212 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈)) |
213 | 212, 3, 23 | srasubrg 31077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵)) |
214 | | subrgsubg 19534 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵)) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵)) |
216 | 215 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵)) |
217 | 110 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod) |
218 | 61 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) =
(Base‘(Scalar‘𝐶))) |
219 | 186, 218 | eleqtrd 2892 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶))) |
220 | 20 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶)) |
221 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
222 | 220, 221 | sseldd 3916 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶)) |
223 | 17, 111, 112, 113 | lmodvscl 19644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖) ∈ (Base‘𝐶)) |
224 | 217, 219,
222, 223 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖) ∈ (Base‘𝐶)) |
225 | 125 | oveqd 7152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖)) |
226 | 225 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐶)𝑖)) |
227 | 32 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶)) |
228 | 224, 226,
227 | 3eltr4d 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) ∈ 𝑈) |
229 | 228 | fmpttd 6856 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)):𝑋⟶𝑈) |
230 | 212, 23 | srasca 19946 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵)) |
231 | 5, 230 | syl5eq 2845 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 = (Scalar‘𝐵)) |
232 | 231 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵)) |
233 | | eqid 2798 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝐵) =
(Base‘𝐵) |
234 | | ovexd 7170 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V) |
235 | 20, 33 | sstrd 3925 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸)) |
236 | 235 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸)) |
237 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋) |
238 | 236, 237 | sseldd 3916 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸)) |
239 | 238 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸)) |
240 | 212, 23 | srabase 19943 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵)) |
241 | 240 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵)) |
242 | 239, 241 | eleqtrd 2892 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵)) |
243 | | eqid 2798 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝐹) = (0g‘𝐹) |
244 | | eqid 2798 |
. . . . . . . . . . . . . . . . . . 19
⊢ (
·𝑠 ‘𝐵) = ( ·𝑠
‘𝐵) |
245 | 144, 209,
232, 233, 234, 242, 204, 243, 244, 181 | mptscmfsupp0 19692 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) finSupp (0g‘𝐵)) |
246 | 204, 211,
144, 216, 229, 245 | gsumsubgcl 19033 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ 𝑈) |
247 | 231 | fveq2d 6649 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (Base‘𝐹) =
(Base‘(Scalar‘𝐵))) |
248 | 25, 247 | eqtrd 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵))) |
249 | 248 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵))) |
250 | 246, 249 | eleqtrd 2892 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵))) |
251 | 250 | fmpttd 6856 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) |
252 | 251 | ffund 6491 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))) |
253 | | fvexd 6660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(0g‘(Scalar‘𝐵)) ∈ V) |
254 | | fconstmpt 5578 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) |
255 | 254 | eqeq2i 2811 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
256 | | ovex 7168 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘𝑊𝑖) ∈ V |
257 | 256 | rgenw 3118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∀𝑖 ∈
𝑋 (𝑘𝑊𝑖) ∈ V |
258 | | mpteqb 6764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑖 ∈
𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
259 | 257, 258 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
260 | 255, 259 | bitri 278 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
261 | 260 | necon3abii 3033 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
262 | | df-ov 7138 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘𝑊𝑖) = (𝑊‘〈𝑘, 𝑖〉) |
263 | 262 | eqcomi 2807 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊‘〈𝑘, 𝑖〉) = (𝑘𝑊𝑖) |
264 | 263 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘〈𝑘, 𝑖〉) = (𝑘𝑊𝑖)) |
265 | 264 | eqeq1d 2800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘〈𝑘, 𝑖〉) =
(0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
266 | 265 | necon3abid 3023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
267 | 266 | rexbidva 3255 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
268 | | rexnal 3201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑖 ∈
𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
269 | 267, 268 | syl6rbb 291 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)))) |
270 | 261, 269 | syl5bb 286 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)))) |
271 | 270 | rabbidva 3425 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴))}) |
272 | | fveq2 6645 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑘, 𝑖〉 → (𝑊‘𝑧) = (𝑊‘〈𝑘, 𝑖〉)) |
273 | 272 | neeq1d 3046 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑘, 𝑖〉 → ((𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴)) ↔ (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴)))) |
274 | 273 | dmrab 30267 |
. . . . . . . . . . . . . . . 16
⊢ dom
{𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘〈𝑘, 𝑖〉) ≠
(0g‘(Scalar‘𝐴))} |
275 | 271, 274 | eqtr4di 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))}) |
276 | | fvexd 6660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(0g‘(Scalar‘𝐴)) ∈ V) |
277 | | suppvalfn 7820 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧
(0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp
(0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))}) |
278 | 157, 147,
276, 277 | syl3anc 1368 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑊 supp
(0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))}) |
279 | 160 | fsuppimpd 8824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑊 supp
(0g‘(Scalar‘𝐴))) ∈ Fin) |
280 | 278, 279 | eqeltrrd 2891 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin) |
281 | | dmfi 8786 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin) |
282 | 280, 281 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠
(0g‘(Scalar‘𝐴))} ∈ Fin) |
283 | 275, 282 | eqeltrd 2890 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} ∈ Fin) |
284 | | nfv 1915 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖𝜑 |
285 | | nfcv 2955 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑖𝑌 |
286 | | nfmpt1 5128 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) |
287 | | nfcv 2955 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑖(𝑋 ×
{(0g‘(Scalar‘𝐴))}) |
288 | 286, 287 | nfne 3087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) |
289 | 288, 285 | nfrabw 3338 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} |
290 | 285, 289 | nfdif 4053 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
291 | 290 | nfcri 2943 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
292 | 284, 291 | nfan 1900 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) |
293 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) |
294 | 293 | eldifad 3893 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌) |
295 | 293 | eldifbd 3894 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
296 | | oveq1 7142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖)) |
297 | 296 | mpteq2dv 5126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
298 | 297 | neeq1d 3046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
299 | 298 | elrab 3628 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
300 | 295, 299 | sylnib 331 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
301 | 294, 300 | mpnanrd 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
302 | | nne 2991 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
303 | 301, 302 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
304 | 303, 254 | eqtrdi 2849 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
305 | | ovex 7168 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗𝑊𝑖) ∈ V |
306 | 305 | rgenw 3118 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
∀𝑖 ∈
𝑋 (𝑗𝑊𝑖) ∈ V |
307 | | mpteqb 6764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑖 ∈
𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
308 | 306, 307 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
309 | 304, 308 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
310 | 309 | r19.21bi 3173 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
311 | 310 | oveq1d 7150 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = ((0g‘(Scalar‘𝐴))(
·𝑠 ‘𝐵)𝑖)) |
312 | 117, 1, 3 | drgext0g 31080 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) |
313 | 117, 1, 3 | drgext0gsca 31082 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0g‘𝐵) =
(0g‘(Scalar‘𝐵))) |
314 | 312, 177,
313 | 3eqtr3d 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐵))) |
315 | 314 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐵))) |
316 | 315 | oveq1d 7150 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) →
((0g‘(Scalar‘𝐴))( ·𝑠
‘𝐵)𝑖) = ((0g‘(Scalar‘𝐵))(
·𝑠 ‘𝐵)𝑖)) |
317 | 208 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod) |
318 | 294, 242 | syldanl 604 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵)) |
319 | | eqid 2798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Scalar‘𝐵) =
(Scalar‘𝐵) |
320 | | eqid 2798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘(Scalar‘𝐵)) =
(0g‘(Scalar‘𝐵)) |
321 | 233, 319,
244, 320, 204 | lmod0vs 19660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) →
((0g‘(Scalar‘𝐵))( ·𝑠
‘𝐵)𝑖) = (0g‘𝐵)) |
322 | 317, 318,
321 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) →
((0g‘(Scalar‘𝐵))( ·𝑠
‘𝐵)𝑖) = (0g‘𝐵)) |
323 | 311, 316,
322 | 3eqtrd 2837 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖) = (0g‘𝐵)) |
324 | 292, 323 | mpteq2da 5124 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) |
325 | 324 | oveq2d 7151 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵)))) |
326 | 208, 210 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ Abel) |
327 | | ablgrp 18903 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp) |
328 | | grpmnd 18102 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd) |
329 | 326, 327,
328 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈ Mnd) |
330 | 204 | gsumz 17992 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵)) |
331 | 329, 16, 330 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵)) |
332 | 331 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵)) |
333 | 313 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (0g‘𝐵) =
(0g‘(Scalar‘𝐵))) |
334 | 325, 332,
333 | 3eqtrd 2837 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
335 | 334, 142 | suppss2 7847 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) supp
(0g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})}) |
336 | | suppssfifsupp 8832 |
. . . . . . . . . . . . . 14
⊢ ((((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ V ∧ Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∧
(0g‘(Scalar‘𝐵)) ∈ V) ∧ ({𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})} ∈ Fin ∧ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) supp
(0g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 ×
{(0g‘(Scalar‘𝐴))})})) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵))) |
337 | 203, 252,
253, 283, 335, 336 | syl32anc 1375 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵))) |
338 | | eqidd 2799 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))) |
339 | | ovexd 7170 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V) |
340 | 338, 339 | fvmpt2d 6758 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
341 | 340 | oveq1d 7150 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
342 | 341 | mpteq2dva 5125 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) |
343 | 342 | oveq2d 7151 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
344 | 119 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐵)) |
345 | 43 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (.r‘𝐸) = (
·𝑠 ‘𝐴)) |
346 | 345 | oveqd 7152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)) |
347 | 346 | mpteq2dva 5125 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖))) |
348 | 118 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = (
·𝑠 ‘𝐵)) |
349 | 348 | oveqd 7152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)) |
350 | 349 | mpteq2dv 5126 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) |
351 | 347, 350 | eqtr3d 2835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) |
352 | 351 | oveq2d 7151 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
353 | | eqidd 2799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗) |
354 | 344, 352,
353 | oveq123d 7156 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
355 | 201 | oveq1d 7150 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
356 | 354, 355 | eqtrd 2833 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)) |
357 | 356 | mpteq2dva 5125 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) |
358 | 357 | oveq2d 7151 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
359 | 10, 21 | sraring 31075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring) |
360 | 162, 36, 359 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ Ring) |
361 | | ringcmn 19327 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd) |
362 | 360, 361 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ CMnd) |
363 | 162 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring) |
364 | | eqid 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(LBasis‘𝐵) =
(LBasis‘𝐵) |
365 | 233, 364 | lbsss 19842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵)) |
366 | 142, 365 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵)) |
367 | 366, 240 | sseqtrrd 3956 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸)) |
368 | 367 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸)) |
369 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌) |
370 | 368, 369 | sseldd 3916 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸)) |
371 | 21, 67 | ringcl 19307 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸)) |
372 | 363, 238,
370, 371 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸)) |
373 | 37 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴)) |
374 | 372, 373 | eleqtrd 2892 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴)) |
375 | 374 | ralrimivva 3156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴)) |
376 | | fedgmullem.d |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗)) |
377 | 376 | fmpo 7748 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑗 ∈
𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴)) |
378 | 375, 377 | sylib 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴)) |
379 | 72, 73, 75, 74, 15, 156, 378, 147 | lcomf 19666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑊 ∘f (
·𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴)) |
380 | 72, 73, 75, 74, 15, 156, 378, 147, 134, 135, 160 | lcomfsupp 19667 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑊 ∘f (
·𝑠 ‘𝐴)𝐷) finSupp (0g‘𝐴)) |
381 | 74, 134, 362, 142, 16, 379, 380 | gsumxp 19089 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖)))))) |
382 | | fedgmullem2.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)) = (0g‘𝐴)) |
383 | 162 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring) |
384 | 156 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))) |
385 | 57, 55 | eqtrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶))) |
386 | 385, 36 | eqsstrrd 3954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 →
(Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸)) |
387 | 61, 386 | eqsstrd 3953 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸)) |
388 | 387, 37 | sseqtrd 3955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 →
(Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴)) |
389 | 388 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴)) |
390 | 384, 389 | fssd 6502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴)) |
391 | | simp2 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌) |
392 | | simp3 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
393 | 390, 391,
392 | fovrnd 7300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴)) |
394 | 37 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴)) |
395 | 393, 394 | eleqtrrd 2893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸)) |
396 | 238 | 3impb 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸)) |
397 | 370 | 3impb 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸)) |
398 | 21, 67 | ringass 19310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) |
399 | 383, 395,
396, 397, 398 | syl13anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) |
400 | 399 | mpoeq3dva 7210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) |
401 | | ovexd 7170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V) |
402 | | ovexd 7170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ V) |
403 | | fnov 7261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
404 | 157, 403 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
405 | 376 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗))) |
406 | 142, 16, 401, 402, 404, 405 | offval22 7766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑊 ∘f
(.r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) |
407 | | ofeq 7391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((.r‘𝐸) = ( ·𝑠
‘𝐴) →
∘f (.r‘𝐸) = ∘f (
·𝑠 ‘𝐴)) |
408 | 43, 407 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ∘f
(.r‘𝐸) =
∘f ( ·𝑠 ‘𝐴)) |
409 | 408 | oveqd 7152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑊 ∘f
(.r‘𝐸)𝐷) = (𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)) |
410 | 400, 406,
409 | 3eqtr2rd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑊 ∘f (
·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) |
411 | 410 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘f (
·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) |
412 | 411 | oveqd 7152 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖)) |
413 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌) |
414 | | ovexd 7170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V) |
415 | | eqid 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
416 | 415 | ovmpt4g 7276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
417 | 413, 221,
414, 416 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
418 | 412, 417 | eqtrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) |
419 | 418 | mpteq2dva 5125 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) |
420 | 419 | oveq2d 7151 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))) |
421 | 162 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring) |
422 | 367 | sselda 3915 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸)) |
423 | 162 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring) |
424 | 386 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸)) |
425 | 424, 219 | sseldd 3916 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸)) |
426 | 21, 67 | ringcl 19307 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸)) |
427 | 423, 425,
239, 426 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸)) |
428 | 312 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐸) = (0g‘𝐵)) |
429 | 245, 350,
428 | 3brtr4d 5062 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) finSupp (0g‘𝐸)) |
430 | 21, 167, 93, 67, 421, 144, 422, 427, 429 | gsummulc1 19352 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗)) |
431 | 420, 430 | eqtrd 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗)) |
432 | 144 | mptexd 6964 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖)) ∈ V) |
433 | 15 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod) |
434 | 36 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸)) |
435 | 10, 432, 194, 433, 434 | gsumsra 30732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖)))) |
436 | 144 | mptexd 6964 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) ∈ V) |
437 | 10, 436, 194, 433, 434 | gsumsra 30732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))) |
438 | 437 | oveq1d 7150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗)) |
439 | 43 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = (
·𝑠 ‘𝐴)) |
440 | 347 | oveq2d 7151 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))) |
441 | 439, 440,
353 | oveq123d 7156 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) |
442 | 438, 441 | eqtrd 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) |
443 | 431, 435,
442 | 3eqtr3d 2841 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)) |
444 | 443 | mpteq2dva 5125 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) |
445 | 444 | oveq2d 7151 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f (
·𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗)))) |
446 | 381, 382,
445 | 3eqtr3rd 2842 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) = (0g‘𝐴)) |
447 | 10, 1, 9 | drgext0g 31080 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐴)) |
448 | 446, 447,
312 | 3eqtr2d 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐴)𝑖)))( ·𝑠
‘𝐴)𝑗))) = (0g‘𝐵)) |
449 | 10, 1, 9, 11, 2, 142 | drgextgsum 31085 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
450 | 117, 1, 3, 5, 104, 142 | drgextgsum 31085 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
451 | 449, 450 | eqtr3d 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗)))) |
452 | 358, 448,
451 | 3eqtr3rd 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) |
453 | 343, 452 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) |
454 | | breq1 5033 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑏 finSupp
(0g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)))) |
455 | | nfmpt1 5128 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
456 | 455 | nfeq2 2972 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) |
457 | | fveq1 6644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)) |
458 | 457 | oveq1d 7150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)) |
459 | 458 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)) |
460 | 456, 459 | mpteq2da 5124 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) |
461 | 460 | oveq2d 7151 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗)))) |
462 | 461 | eqeq1d 2800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → ((𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵) ↔ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵))) |
463 | 454, 462 | anbi12d 633 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → ((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)))) |
464 | | eqeq1 2802 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
465 | 463, 464 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) → (((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))})) ↔ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))})))) |
466 | 364 | lbslinds 20522 |
. . . . . . . . . . . . . . . 16
⊢
(LBasis‘𝐵)
⊆ (LIndS‘𝐵) |
467 | 466, 142 | sseldi 3913 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵)) |
468 | | eqid 2798 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵)) |
469 | 233, 468,
319, 244, 204, 320 | islinds5 30983 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))})))) |
470 | 469 | biimpa 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
471 | 208, 366,
467, 470 | syl21anc 836 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
472 | | fvexd 6660 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Base‘(Scalar‘𝐵)) ∈ V) |
473 | | elmapg 8402 |
. . . . . . . . . . . . . . . 16
⊢
(((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))) |
474 | 473 | biimpar 481 |
. . . . . . . . . . . . . . 15
⊢
((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)) |
475 | 472, 142,
251, 474 | syl21anc 836 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)) |
476 | 465, 471,
475 | rspcdva 3573 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) finSupp
(0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))))‘𝑗)( ·𝑠
‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))}))) |
477 | 337, 453,
476 | mp2and 698 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑌 ×
{(0g‘(Scalar‘𝐵))})) |
478 | | fconstmpt 5578 |
. . . . . . . . . . . 12
⊢ (𝑌 ×
{(0g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵))) |
479 | 477, 478 | eqtrdi 2849 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵)))) |
480 | | ovex 7168 |
. . . . . . . . . . . . 13
⊢ (𝐵 Σg
(𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V |
481 | 480 | rgenw 3118 |
. . . . . . . . . . . 12
⊢
∀𝑗 ∈
𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V |
482 | | mpteqb 6764 |
. . . . . . . . . . . 12
⊢
(∀𝑗 ∈
𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) ∈ V → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵)))) |
483 | 481, 482 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦
(0g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
484 | 479, 483 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
485 | 484 | r19.21bi 3173 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠
‘𝐵)𝑖))) =
(0g‘(Scalar‘𝐵))) |
486 | 312, 447,
313 | 3eqtr3rd 2842 |
. . . . . . . . . 10
⊢ (𝜑 →
(0g‘(Scalar‘𝐵)) = (0g‘𝐴)) |
487 | 486 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) →
(0g‘(Scalar‘𝐵)) = (0g‘𝐴)) |
488 | 202, 485,
487 | 3eqtrd 2837 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) |
489 | 183, 488 | jca 515 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴))) |
490 | 186 | fmpttd 6856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))) |
491 | | fvexd 6660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V) |
492 | 491, 144 | elmapd 8403 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))) |
493 | 490, 492 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)) |
494 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
495 | 494 | breq1d 5040 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp
(0g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)))) |
496 | | nfv 1915 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌) |
497 | | nfmpt1 5128 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) |
498 | 497 | nfeq2 2972 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) |
499 | 496, 498 | nfan 1900 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
500 | | simplr 768 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) |
501 | 500 | fveq1d 6647 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)) |
502 | 501 | oveq1d 7150 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖)) |
503 | 499, 502 | mpteq2da 5124 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) |
504 | 503 | oveq2d 7151 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖)))) |
505 | 504 | eqeq1d 2800 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴) ↔ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴))) |
506 | 495, 505 | anbi12d 633 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)))) |
507 | 494 | eqeq1d 2800 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))}))) |
508 | 506, 507 | imbi12d 348 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) ↔ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})))) |
509 | 493, 508 | rspcdv 3563 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp
(0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠
‘𝐴)𝑖))) = (0g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})))) |
510 | 139, 489,
509 | mp2d 49 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 ×
{(0g‘(Scalar‘𝐴))})) |
511 | 510, 254 | eqtrdi 2849 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
512 | 511, 308 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
513 | 512 | ralrimiva 3149 |
. . 3
⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))) |
514 | | eqidd 2799 |
. . . 4
⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) →
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐴))) |
515 | | fvexd 6660 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) →
(0g‘(Scalar‘𝐴)) ∈ V) |
516 | | fvexd 6660 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) →
(0g‘(Scalar‘𝐴)) ∈ V) |
517 | 157, 514,
515, 516 | fnmpoovd 7765 |
. . 3
⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))) |
518 | 513, 517 | mpbird 260 |
. 2
⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴)))) |
519 | | fconstmpo 7248 |
. 2
⊢ ((𝑌 × 𝑋) ×
{(0g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦
(0g‘(Scalar‘𝐴))) |
520 | 518, 519 | eqtr4di 2851 |
1
⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) ×
{(0g‘(Scalar‘𝐴))})) |