Step |
Hyp |
Ref |
Expression |
1 |
|
imasbas.u |
⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) ) |
2 |
|
imasbas.v |
⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) |
3 |
|
imasbas.f |
⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 ) |
4 |
|
imasbas.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝑍 ) |
5 |
|
imassca.g |
⊢ 𝐺 = ( Scalar ‘ 𝑅 ) |
6 |
|
imasvsca.k |
⊢ 𝐾 = ( Base ‘ 𝐺 ) |
7 |
|
imasvsca.q |
⊢ · = ( ·𝑠 ‘ 𝑅 ) |
8 |
|
imasvsca.s |
⊢ ∙ = ( ·𝑠 ‘ 𝑈 ) |
9 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
10 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
11 |
|
eqid |
⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 ) |
12 |
5
|
fveq2i |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( Scalar ‘ 𝑅 ) ) |
13 |
6 12
|
eqtri |
⊢ 𝐾 = ( Base ‘ ( Scalar ‘ 𝑅 ) ) |
14 |
|
eqid |
⊢ ( ·𝑖 ‘ 𝑅 ) = ( ·𝑖 ‘ 𝑅 ) |
15 |
|
eqid |
⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 ) |
16 |
|
eqid |
⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 ) |
17 |
|
eqid |
⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 ) |
18 |
|
eqid |
⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 ) |
19 |
1 2 3 4 9 18
|
imasplusg |
⊢ ( 𝜑 → ( +g ‘ 𝑈 ) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) 〉 } ) |
20 |
|
eqid |
⊢ ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 ) |
21 |
1 2 3 4 10 20
|
imasmulr |
⊢ ( 𝜑 → ( .r ‘ 𝑈 ) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) 〉 } ) |
22 |
|
eqidd |
⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) |
23 |
|
eqidd |
⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } ) |
24 |
|
eqidd |
⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ) |
25 |
|
eqid |
⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 ) |
26 |
1 2 3 4 16 25
|
imasds |
⊢ ( 𝜑 → ( dist ‘ 𝑈 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑢 ∈ ℕ ran ( 𝑧 ∈ { 𝑤 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑢 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( 𝑤 ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑤 ‘ 𝑢 ) ) ) = 𝑦 ∧ ∀ 𝑣 ∈ ( 1 ... ( 𝑢 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑤 ‘ 𝑣 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑤 ‘ ( 𝑣 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑧 ) ) ) , ℝ* , < ) ) ) |
27 |
|
eqidd |
⊢ ( 𝜑 → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) = ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ) |
28 |
1 2 9 10 11 13 7 14 15 16 17 19 21 22 23 24 26 27 3 4
|
imasval |
⊢ ( 𝜑 → 𝑈 = ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) 〉 , 〈 ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) 〉 , 〈 ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) 〉 } ) ) |
29 |
|
eqid |
⊢ ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) 〉 , 〈 ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) 〉 , 〈 ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) 〉 } ) = ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) 〉 , 〈 ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) 〉 , 〈 ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) 〉 } ) |
30 |
29
|
imasvalstr |
⊢ ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) 〉 , 〈 ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) 〉 , 〈 ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) 〉 } ) Struct 〈 1 , ; 1 2 〉 |
31 |
|
vscaid |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx ) |
32 |
|
snsstp2 |
⊢ { 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 } ⊆ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } |
33 |
|
ssun2 |
⊢ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ⊆ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) |
34 |
|
ssun1 |
⊢ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ⊆ ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) 〉 , 〈 ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) 〉 , 〈 ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) 〉 } ) |
35 |
33 34
|
sstri |
⊢ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ⊆ ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) 〉 , 〈 ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) 〉 , 〈 ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) 〉 } ) |
36 |
32 35
|
sstri |
⊢ { 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 } ⊆ ( ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) 〉 , 〈 ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) 〉 } 〉 } ) ∪ { 〈 ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) 〉 , 〈 ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) 〉 , 〈 ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) 〉 } ) |
37 |
|
fvex |
⊢ ( Base ‘ 𝑅 ) ∈ V |
38 |
2 37
|
eqeltrdi |
⊢ ( 𝜑 → 𝑉 ∈ V ) |
39 |
6
|
fvexi |
⊢ 𝐾 ∈ V |
40 |
|
snex |
⊢ { ( 𝐹 ‘ 𝑞 ) } ∈ V |
41 |
39 40
|
mpoex |
⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V |
42 |
41
|
rgenw |
⊢ ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V |
43 |
|
iunexg |
⊢ ( ( 𝑉 ∈ V ∧ ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V ) → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V ) |
44 |
38 42 43
|
sylancl |
⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V ) |
45 |
28 30 31 36 44 8
|
strfv3 |
⊢ ( 𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) |