Metamath Proof Explorer

Theorem imasvscafn

Description: The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasvscaf.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasvscaf.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasvscaf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasvscaf.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
imasvscaf.g ⊢ 𝐺 = ( Scalar ‘ 𝑅 )
imasvscaf.k ⊢ 𝐾 = ( Base ‘ 𝐺 )
imasvscaf.q ⊢ · = ( ·𝑠 ‘ 𝑅 )
imasvscaf.s ⊢ ∙ = ( ·𝑠 ‘ 𝑈 )
imasvscaf.e ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
Assertion imasvscafn ( 𝜑 → ∙ Fn ( 𝐾 × 𝐵 ) )

Proof

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 eqid ⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
11 fvex ⊢ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ V
12 10 11 fnmpoi ⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) Fn ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } )
13 fnrel ⊢ ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) Fn ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) → Rel ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
14 12 13 ax-mp ⊢ Rel ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
15 14 rgenw ⊢ ∀ 𝑞 ∈ 𝑉 Rel ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
16 reliun ⊢ ( Rel ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ↔ ∀ 𝑞 ∈ 𝑉 Rel ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
17 15 16 mpbir ⊢ Rel ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
18 1 2 3 4 5 6 7 8 imasvsca ⊢ ( 𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
19 18 releqd ⊢ ( 𝜑 → ( Rel ∙ ↔ Rel ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) )
20 17 19 mpbiri ⊢ ( 𝜑 → Rel ∙ )
21 dffn2 ⊢ ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) Fn ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ↔ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⟶ V )
22 12 21 mpbi ⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⟶ V
23 fssxp ⊢ ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⟶ V → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × V ) )
24 22 23 ax-mp ⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × V )
25 fof ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
26 3 25 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
27 26 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 )
28 27 snssd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → { ( 𝐹 ‘ 𝑞 ) } ⊆ 𝐵 )
29 xpss2 ⊢ ( { ( 𝐹 ‘ 𝑞 ) } ⊆ 𝐵 → ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⊆ ( 𝐾 × 𝐵 ) )
30 xpss1 ⊢ ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⊆ ( 𝐾 × 𝐵 ) → ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × V ) ⊆ ( ( 𝐾 × 𝐵 ) × V ) )
31 28 29 30 3syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × V ) ⊆ ( ( 𝐾 × 𝐵 ) × V ) )
32 24 31 sstrid ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × V ) )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × V ) )
34 iunss ⊢ ( ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × V ) ↔ ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × V ) )
35 33 34 sylibr ⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × V ) )
36 18 35 eqsstrd ⊢ ( 𝜑 → ∙ ⊆ ( ( 𝐾 × 𝐵 ) × V ) )
37 dmss ⊢ ( ∙ ⊆ ( ( 𝐾 × 𝐵 ) × V ) → dom ∙ ⊆ dom ( ( 𝐾 × 𝐵 ) × V ) )
38 36 37 syl ⊢ ( 𝜑 → dom ∙ ⊆ dom ( ( 𝐾 × 𝐵 ) × V ) )
39 vn0 ⊢ V ≠ ∅
40 dmxp ⊢ ( V ≠ ∅ → dom ( ( 𝐾 × 𝐵 ) × V ) = ( 𝐾 × 𝐵 ) )
41 39 40 ax-mp ⊢ dom ( ( 𝐾 × 𝐵 ) × V ) = ( 𝐾 × 𝐵 )
42 38 41 sseqtrdi ⊢ ( 𝜑 → dom ∙ ⊆ ( 𝐾 × 𝐵 ) )
43 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
44 3 43 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
45 44 xpeq2d ⊢ ( 𝜑 → ( 𝐾 × ran 𝐹 ) = ( 𝐾 × 𝐵 ) )
46 42 45 sseqtrrd ⊢ ( 𝜑 → dom ∙ ⊆ ( 𝐾 × ran 𝐹 ) )
47 df-br ⊢ ( ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 ↔ ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∙ )
48 18 eleq2d ⊢ ( 𝜑 → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∙ ↔ ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∙ ↔ ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) )
50 eliun ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ↔ ∃ 𝑞 ∈ 𝑉 ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
51 df-3an ⊢ ( ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ↔ ( ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑞 ∈ 𝑉 ) )
52 10 mpofun ⊢ Fun ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
53 funopfv ⊢ ( Fun ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ‘ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ) = 𝑤 ) )
54 52 53 ax-mp ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ‘ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ) = 𝑤 )
55 df-ov ⊢ ( 𝑝 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ( 𝐹 ‘ 𝑎 ) ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ‘ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ )
56 opex ⊢ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∈ V
57 vex ⊢ 𝑤 ∈ V
58 56 57 opeldm ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∈ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
59 10 11 dmmpo ⊢ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } )
60 58 59 eleqtrdi ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) )
61 opelxp ⊢ ( ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ↔ ( 𝑝 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑎 ) ∈ { ( 𝐹 ‘ 𝑞 ) } ) )
62 60 61 sylib ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ( 𝑝 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑎 ) ∈ { ( 𝐹 ‘ 𝑞 ) } ) )
63 fvoveq1 ⊢ ( 𝑧 = 𝑝 → ( 𝐹 ‘ ( 𝑧 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
64 eqidd ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
65 fvoveq1 ⊢ ( 𝑝 = 𝑧 → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑧 · 𝑞 ) ) )
66 eqidd ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ ( 𝑧 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑧 · 𝑞 ) ) )
67 65 66 cbvmpov ⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝑧 ∈ 𝐾 , 𝑦 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑧 · 𝑞 ) ) )
68 63 64 67 11 ovmpo ⊢ ( ( 𝑝 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑎 ) ∈ { ( 𝐹 ‘ 𝑞 ) } ) → ( 𝑝 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
69 62 68 syl ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ( 𝑝 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
70 55 69 eqtr3id ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ‘ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
71 54 70 eqtr3d ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
72 71 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) ∧ ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
73 elsni ⊢ ( ( 𝐹 ‘ 𝑎 ) ∈ { ( 𝐹 ‘ 𝑞 ) } → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) )
74 62 73 simpl2im ⊢ ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) )
75 9 74 impel ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) ∧ ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
76 72 75 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) ∧ ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) )
77 76 ex ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
78 51 77 sylan2br ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑞 ∈ 𝑉 ) ) → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
79 78 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑞 ∈ 𝑉 ) → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
80 79 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) → ( ∃ 𝑞 ∈ 𝑉 ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
81 50 80 syl5bi ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
82 49 81 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) → ( ⟨ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ , 𝑤 ⟩ ∈ ∙ → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
83 47 82 syl5bi ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) → ( ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
84 83 alrimiv ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) → ∀ 𝑤 ( ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) )
85 mo2icl ⊢ ( ∀ 𝑤 ( ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 → 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) ) → ∃* 𝑤 ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 )
86 84 85 syl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ) ) → ∃* 𝑤 ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 )
87 86 ralrimivva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐾 ∀ 𝑎 ∈ 𝑉 ∃* 𝑤 ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 )
88 fofn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 Fn 𝑉 )
89 opeq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ⟨ 𝑝 , 𝑦 ⟩ = ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ )
90 89 breq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 ↔ ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 ) )
91 90 mobidv ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ∃* 𝑤 ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 ↔ ∃* 𝑤 ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 ) )
92 91 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 ↔ ∀ 𝑎 ∈ 𝑉 ∃* 𝑤 ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 ) )
93 3 88 92 3syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 ↔ ∀ 𝑎 ∈ 𝑉 ∃* 𝑤 ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 ) )
94 93 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐾 ∀ 𝑦 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 ↔ ∀ 𝑝 ∈ 𝐾 ∀ 𝑎 ∈ 𝑉 ∃* 𝑤 ⟨ 𝑝 , ( 𝐹 ‘ 𝑎 ) ⟩ ∙ 𝑤 ) )
95 87 94 mpbird ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐾 ∀ 𝑦 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 )
96 breq1 ⊢ ( 𝑥 = ⟨ 𝑝 , 𝑦 ⟩ → ( 𝑥 ∙ 𝑤 ↔ ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 ) )
97 96 mobidv ⊢ ( 𝑥 = ⟨ 𝑝 , 𝑦 ⟩ → ( ∃* 𝑤 𝑥 ∙ 𝑤 ↔ ∃* 𝑤 ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 ) )
98 97 ralxp ⊢ ( ∀ 𝑥 ∈ ( 𝐾 × ran 𝐹 ) ∃* 𝑤 𝑥 ∙ 𝑤 ↔ ∀ 𝑝 ∈ 𝐾 ∀ 𝑦 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑝 , 𝑦 ⟩ ∙ 𝑤 )
99 95 98 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐾 × ran 𝐹 ) ∃* 𝑤 𝑥 ∙ 𝑤 )
100 ssralv ⊢ ( dom ∙ ⊆ ( 𝐾 × ran 𝐹 ) → ( ∀ 𝑥 ∈ ( 𝐾 × ran 𝐹 ) ∃* 𝑤 𝑥 ∙ 𝑤 → ∀ 𝑥 ∈ dom ∙ ∃* 𝑤 𝑥 ∙ 𝑤 ) )
101 46 99 100 sylc ⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ∙ ∃* 𝑤 𝑥 ∙ 𝑤 )
102 dffun7 ⊢ ( Fun ∙ ↔ ( Rel ∙ ∧ ∀ 𝑥 ∈ dom ∙ ∃* 𝑤 𝑥 ∙ 𝑤 ) )
103 20 101 102 sylanbrc ⊢ ( 𝜑 → Fun ∙ )
104 eqimss2 ⊢ ( ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ )
105 18 104 syl ⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ )
106 iunss ⊢ ( ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ ↔ ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ )
107 105 106 sylib ⊢ ( 𝜑 → ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ )
108 107 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ )
109 108 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ )
110 dmss ⊢ ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ∙ → dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ dom ∙ )
111 109 110 syl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ dom ∙ )
112 59 111 eqsstrrid ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⊆ dom ∙ )
113 simprl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → 𝑝 ∈ 𝐾 )
114 fvex ⊢ ( 𝐹 ‘ 𝑞 ) ∈ V
115 114 snid ⊢ ( 𝐹 ‘ 𝑞 ) ∈ { ( 𝐹 ‘ 𝑞 ) }
116 opelxpi ⊢ ( ( 𝑝 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑞 ) ∈ { ( 𝐹 ‘ 𝑞 ) } ) → ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) )
117 113 115 116 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) )
118 112 117 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
119 118 ralrimivva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐾 ∀ 𝑞 ∈ 𝑉 ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
120 opeq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑞 ) → ⟨ 𝑝 , 𝑦 ⟩ = ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ )
121 120 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑞 ) → ( ⟨ 𝑝 , 𝑦 ⟩ ∈ dom ∙ ↔ ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
122 121 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ⟨ 𝑝 , 𝑦 ⟩ ∈ dom ∙ ↔ ∀ 𝑞 ∈ 𝑉 ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
123 3 88 122 3syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ⟨ 𝑝 , 𝑦 ⟩ ∈ dom ∙ ↔ ∀ 𝑞 ∈ 𝑉 ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
124 123 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐾 ∀ 𝑦 ∈ ran 𝐹 ⟨ 𝑝 , 𝑦 ⟩ ∈ dom ∙ ↔ ∀ 𝑝 ∈ 𝐾 ∀ 𝑞 ∈ 𝑉 ⟨ 𝑝 , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
125 119 124 mpbird ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐾 ∀ 𝑦 ∈ ran 𝐹 ⟨ 𝑝 , 𝑦 ⟩ ∈ dom ∙ )
126 eleq1 ⊢ ( 𝑥 = ⟨ 𝑝 , 𝑦 ⟩ → ( 𝑥 ∈ dom ∙ ↔ ⟨ 𝑝 , 𝑦 ⟩ ∈ dom ∙ ) )
127 126 ralxp ⊢ ( ∀ 𝑥 ∈ ( 𝐾 × ran 𝐹 ) 𝑥 ∈ dom ∙ ↔ ∀ 𝑝 ∈ 𝐾 ∀ 𝑦 ∈ ran 𝐹 ⟨ 𝑝 , 𝑦 ⟩ ∈ dom ∙ )
128 125 127 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐾 × ran 𝐹 ) 𝑥 ∈ dom ∙ )
129 dfss3 ⊢ ( ( 𝐾 × ran 𝐹 ) ⊆ dom ∙ ↔ ∀ 𝑥 ∈ ( 𝐾 × ran 𝐹 ) 𝑥 ∈ dom ∙ )
130 128 129 sylibr ⊢ ( 𝜑 → ( 𝐾 × ran 𝐹 ) ⊆ dom ∙ )
131 45 130 eqsstrrd ⊢ ( 𝜑 → ( 𝐾 × 𝐵 ) ⊆ dom ∙ )
132 42 131 eqssd ⊢ ( 𝜑 → dom ∙ = ( 𝐾 × 𝐵 ) )
133 df-fn ⊢ ( ∙ Fn ( 𝐾 × 𝐵 ) ↔ ( Fun ∙ ∧ dom ∙ = ( 𝐾 × 𝐵 ) ) )
134 103 132 133 sylanbrc ⊢ ( 𝜑 → ∙ Fn ( 𝐾 × 𝐵 ) )