Step |
Hyp |
Ref |
Expression |
1 |
|
imasvscaf.u |
⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) ) |
2 |
|
imasvscaf.v |
⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) |
3 |
|
imasvscaf.f |
⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 ) |
4 |
|
imasvscaf.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝑍 ) |
5 |
|
imasvscaf.g |
⊢ 𝐺 = ( Scalar ‘ 𝑅 ) |
6 |
|
imasvscaf.k |
⊢ 𝐾 = ( Base ‘ 𝐺 ) |
7 |
|
imasvscaf.q |
⊢ · = ( ·𝑠 ‘ 𝑅 ) |
8 |
|
imasvscaf.s |
⊢ ∙ = ( ·𝑠 ‘ 𝑈 ) |
9 |
|
imasvscaf.e |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) |
10 |
1 2 3 4 5 6 7 8 9
|
imasvscafn |
⊢ ( 𝜑 → ∙ Fn ( 𝐾 × 𝐵 ) ) |
11 |
|
fnfun |
⊢ ( ∙ Fn ( 𝐾 × 𝐵 ) → Fun ∙ ) |
12 |
10 11
|
syl |
⊢ ( 𝜑 → Fun ∙ ) |
13 |
12
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → Fun ∙ ) |
14 |
|
eqidd |
⊢ ( 𝑞 = 𝑌 → 𝐾 = 𝐾 ) |
15 |
|
fveq2 |
⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑌 ) ) |
16 |
15
|
sneqd |
⊢ ( 𝑞 = 𝑌 → { ( 𝐹 ‘ 𝑞 ) } = { ( 𝐹 ‘ 𝑌 ) } ) |
17 |
|
oveq2 |
⊢ ( 𝑞 = 𝑌 → ( 𝑝 · 𝑞 ) = ( 𝑝 · 𝑌 ) ) |
18 |
17
|
fveq2d |
⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) |
19 |
14 16 18
|
mpoeq123dv |
⊢ ( 𝑞 = 𝑌 → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ) |
20 |
19
|
ssiun2s |
⊢ ( 𝑌 ∈ 𝑉 → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) |
21 |
20
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) |
22 |
1 2 3 4 5 6 7 8
|
imasvsca |
⊢ ( 𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) |
23 |
22
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) |
24 |
21 23
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∙ ) |
25 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝐾 ) |
26 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑌 ) ∈ V |
27 |
26
|
snid |
⊢ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) } |
28 |
|
opelxpi |
⊢ ( ( 𝑋 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) } ) → 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } ) ) |
29 |
25 27 28
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } ) ) |
30 |
|
eqid |
⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) |
31 |
|
fvex |
⊢ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ∈ V |
32 |
30 31
|
dmmpo |
⊢ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) = ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } ) |
33 |
29 32
|
eleqtrrdi |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ∈ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ) |
34 |
|
funssfv |
⊢ ( ( Fun ∙ ∧ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∙ ∧ 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ∈ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ) → ( ∙ ‘ 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ) ) |
35 |
13 24 33 34
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( ∙ ‘ 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ) ) |
36 |
|
df-ov |
⊢ ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( ∙ ‘ 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ) |
37 |
|
df-ov |
⊢ ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ 〈 𝑋 , ( 𝐹 ‘ 𝑌 ) 〉 ) |
38 |
35 36 37
|
3eqtr4g |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) ) |
39 |
|
fvoveq1 |
⊢ ( 𝑝 = 𝑋 → ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) |
40 |
|
eqidd |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑌 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) |
41 |
|
fvex |
⊢ ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ∈ V |
42 |
39 40 30 41
|
ovmpo |
⊢ ( ( 𝑋 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) } ) → ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) |
43 |
25 27 42
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) |
44 |
38 43
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) |