Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
2 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐹‘(𝑝 · 𝑞)) ∈ V |
3 | 1, 2 | fnmpt2i 7239 |
. . . . . . 7
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹‘𝑞)}) |
4 | | fnrel 5989 |
. . . . . . 7
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹‘𝑞)}) → Rel (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢ Rel
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
6 | 5 | rgenw 2924 |
. . . . 5
⊢
∀𝑞 ∈
𝑉 Rel (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
7 | | reliun 5239 |
. . . . 5
⊢ (Rel
∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ↔ ∀𝑞 ∈ 𝑉 Rel (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
8 | 6, 7 | mpbir 221 |
. . . 4
⊢ Rel
∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
9 | | imasvscaf.u |
. . . . . 6
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
10 | | imasvscaf.v |
. . . . . 6
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
11 | | imasvscaf.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
12 | | imasvscaf.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ 𝑍) |
13 | | imasvscaf.g |
. . . . . 6
⊢ 𝐺 = (Scalar‘𝑅) |
14 | | imasvscaf.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝐺) |
15 | | imasvscaf.q |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑅) |
16 | | imasvscaf.s |
. . . . . 6
⊢ ∙ = (
·𝑠 ‘𝑈) |
17 | 9, 10, 11, 12, 13, 14, 15, 16 | imasvsca 16180 |
. . . . 5
⊢ (𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
18 | 17 | releqd 5203 |
. . . 4
⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))) |
19 | 8, 18 | mpbiri 248 |
. . 3
⊢ (𝜑 → Rel ∙ ) |
20 | | dffn2 6047 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹‘𝑞)}) ↔ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹‘𝑞)})⟶V) |
21 | 3, 20 | mpbi 220 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹‘𝑞)})⟶V |
22 | | fssxp 6060 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹‘𝑞)})⟶V → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × {(𝐹‘𝑞)}) × V)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × {(𝐹‘𝑞)}) × V) |
24 | | fof 6115 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
25 | 11, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
26 | 25 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵) |
27 | 26 | snssd 4340 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → {(𝐹‘𝑞)} ⊆ 𝐵) |
28 | | xpss2 5229 |
. . . . . . . . . . . 12
⊢ ({(𝐹‘𝑞)} ⊆ 𝐵 → (𝐾 × {(𝐹‘𝑞)}) ⊆ (𝐾 × 𝐵)) |
29 | | xpss1 5228 |
. . . . . . . . . . . 12
⊢ ((𝐾 × {(𝐹‘𝑞)}) ⊆ (𝐾 × 𝐵) → ((𝐾 × {(𝐹‘𝑞)}) × V) ⊆ ((𝐾 × 𝐵) × V)) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → ((𝐾 × {(𝐹‘𝑞)}) × V) ⊆ ((𝐾 × 𝐵) × V)) |
31 | 23, 30 | syl5ss 3614 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
32 | 31 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
33 | | iunss 4561 |
. . . . . . . . 9
⊢ (∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V) ↔ ∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
34 | 32, 33 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
35 | 17, 34 | eqsstrd 3639 |
. . . . . . 7
⊢ (𝜑 → ∙ ⊆ ((𝐾 × 𝐵) × V)) |
36 | | dmss 5323 |
. . . . . . 7
⊢ ( ∙
⊆ ((𝐾 × 𝐵) × V) → dom ∙
⊆ dom ((𝐾 ×
𝐵) ×
V)) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom ∙ ⊆ dom ((𝐾 × 𝐵) × V)) |
38 | | vn0 3924 |
. . . . . . 7
⊢ V ≠
∅ |
39 | | dmxp 5344 |
. . . . . . 7
⊢ (V ≠
∅ → dom ((𝐾
× 𝐵) × V) =
(𝐾 × 𝐵)) |
40 | 38, 39 | ax-mp 5 |
. . . . . 6
⊢ dom
((𝐾 × 𝐵) × V) = (𝐾 × 𝐵) |
41 | 37, 40 | syl6sseq 3651 |
. . . . 5
⊢ (𝜑 → dom ∙ ⊆ (𝐾 × 𝐵)) |
42 | | forn 6118 |
. . . . . . 7
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) |
43 | 11, 42 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 = 𝐵) |
44 | 43 | xpeq2d 5139 |
. . . . 5
⊢ (𝜑 → (𝐾 × ran 𝐹) = (𝐾 × 𝐵)) |
45 | 41, 44 | sseqtr4d 3642 |
. . . 4
⊢ (𝜑 → dom ∙ ⊆ (𝐾 × ran 𝐹)) |
46 | | df-br 4654 |
. . . . . . . . . 10
⊢
(〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 ↔ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ ) |
47 | 17 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ ↔
〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))) |
48 | 47 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ ↔
〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))) |
49 | | eliun 4524 |
. . . . . . . . . . . 12
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ↔ ∃𝑞 ∈ 𝑉 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
50 | | df-3an 1039 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉) ↔ ((𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉)) |
51 | 1 | mpt2fun 6762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Fun
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
52 | | funopfv 6235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Fun
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) = 𝑤)) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) = 𝑤) |
54 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹‘𝑎)) = ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) |
55 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
〈𝑝, (𝐹‘𝑎)〉 ∈ V |
56 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑤 ∈ V |
57 | 55, 56 | opeldm 5328 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 〈𝑝, (𝐹‘𝑎)〉 ∈ dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
58 | 1, 2 | dmmpt2 7240 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝐾 × {(𝐹‘𝑞)}) |
59 | 57, 58 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 〈𝑝, (𝐹‘𝑎)〉 ∈ (𝐾 × {(𝐹‘𝑞)})) |
60 | | opelxp 5146 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝑝, (𝐹‘𝑎)〉 ∈ (𝐾 × {(𝐹‘𝑞)}) ↔ (𝑝 ∈ 𝐾 ∧ (𝐹‘𝑎) ∈ {(𝐹‘𝑞)})) |
61 | 59, 60 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝑝 ∈ 𝐾 ∧ (𝐹‘𝑎) ∈ {(𝐹‘𝑞)})) |
62 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑝 → (𝑧 · 𝑞) = (𝑝 · 𝑞)) |
63 | 62 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑝 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑝 · 𝑞))) |
64 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝐹‘𝑎) → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑝 · 𝑞))) |
65 | 63 | equcoms 1947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = 𝑧 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑝 · 𝑞))) |
66 | 65 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = 𝑧 → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑧 · 𝑞))) |
67 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑧 · 𝑞))) |
68 | 66, 67 | cbvmpt2v 6735 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝑧 ∈ 𝐾, 𝑦 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑧 · 𝑞))) |
69 | 63, 64, 68, 2 | ovmpt2 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ 𝐾 ∧ (𝐹‘𝑎) ∈ {(𝐹‘𝑞)}) → (𝑝(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹‘𝑎)) = (𝐹‘(𝑝 · 𝑞))) |
70 | 61, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝑝(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹‘𝑎)) = (𝐹‘(𝑝 · 𝑞))) |
71 | 54, 70 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) = (𝐹‘(𝑝 · 𝑞))) |
72 | 53, 71 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑞))) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) ∧ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → 𝑤 = (𝐹‘(𝑝 · 𝑞))) |
74 | 61 | simprd 479 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝐹‘𝑎) ∈ {(𝐹‘𝑞)}) |
75 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑎) ∈ {(𝐹‘𝑞)} → (𝐹‘𝑎) = (𝐹‘𝑞)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝐹‘𝑎) = (𝐹‘𝑞)) |
77 | | imasvscaf.e |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))) |
78 | 77 | imp 445 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) ∧ (𝐹‘𝑎) = (𝐹‘𝑞)) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))) |
79 | 76, 78 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) ∧ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))) |
80 | 73, 79 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) ∧ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → 𝑤 = (𝐹‘(𝑝 · 𝑎))) |
81 | 80 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
82 | 50, 81 | sylan2br 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
83 | 82 | anassrs 680 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑞 ∈ 𝑉) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
84 | 83 | rexlimdva 3031 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (∃𝑞 ∈ 𝑉 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
85 | 49, 84 | syl5bi 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
86 | 48, 85 | sylbid 230 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
87 | 46, 86 | syl5bi 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
88 | 87 | alrimiv 1855 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → ∀𝑤(〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
89 | | mo2icl 3385 |
. . . . . . . 8
⊢
(∀𝑤(〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑝 · 𝑎))) → ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤) |
90 | 88, 89 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤) |
91 | 90 | ralrimivva 2971 |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤) |
92 | | fofn 6117 |
. . . . . . . 8
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉) |
93 | | opeq2 4403 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑎) → 〈𝑝, 𝑦〉 = 〈𝑝, (𝐹‘𝑎)〉) |
94 | 93 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑎) → (〈𝑝, 𝑦〉 ∙ 𝑤 ↔ 〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
95 | 94 | mobidv 2491 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑎) → (∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
96 | 95 | ralrn 6362 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
97 | 11, 92, 96 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
98 | 97 | ralbidv 2986 |
. . . . . 6
⊢ (𝜑 → (∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∀𝑝 ∈ 𝐾 ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
99 | 91, 98 | mpbird 247 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤) |
100 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = 〈𝑝, 𝑦〉 → (𝑥 ∙ 𝑤 ↔ 〈𝑝, 𝑦〉 ∙ 𝑤)) |
101 | 100 | mobidv 2491 |
. . . . . 6
⊢ (𝑥 = 〈𝑝, 𝑦〉 → (∃*𝑤 𝑥 ∙ 𝑤 ↔ ∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤)) |
102 | 101 | ralxp 5263 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐾 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤) |
103 | 99, 102 | sylibr 224 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐾 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤) |
104 | | ssralv 3666 |
. . . 4
⊢ (dom
∙
⊆ (𝐾 × ran
𝐹) → (∀𝑥 ∈ (𝐾 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
105 | 45, 103, 104 | sylc 65 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤) |
106 | | dffun7 5915 |
. . 3
⊢ (Fun
∙
↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
107 | 19, 105, 106 | sylanbrc 698 |
. 2
⊢ (𝜑 → Fun ∙ ) |
108 | | eqimss2 3658 |
. . . . . . . . . . . . . . 15
⊢ ( ∙ =
∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
109 | 17, 108 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
110 | | iunss 4561 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ↔
∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
111 | 109, 110 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
112 | 111 | r19.21bi 2932 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
113 | 112 | adantrl 752 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
114 | | dmss 5323 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ → dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ dom ∙ ) |
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ dom ∙ ) |
116 | 58, 115 | syl5eqssr 3650 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → (𝐾 × {(𝐹‘𝑞)}) ⊆ dom ∙ ) |
117 | | simprl 794 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → 𝑝 ∈ 𝐾) |
118 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑞) ∈ V |
119 | 118 | snid 4208 |
. . . . . . . . . 10
⊢ (𝐹‘𝑞) ∈ {(𝐹‘𝑞)} |
120 | | opelxpi 5148 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ 𝐾 ∧ (𝐹‘𝑞) ∈ {(𝐹‘𝑞)}) → 〈𝑝, (𝐹‘𝑞)〉 ∈ (𝐾 × {(𝐹‘𝑞)})) |
121 | 117, 119,
120 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → 〈𝑝, (𝐹‘𝑞)〉 ∈ (𝐾 × {(𝐹‘𝑞)})) |
122 | 116, 121 | sseldd 3604 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ ) |
123 | 122 | ralrimivva 2971 |
. . . . . . 7
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ ) |
124 | | opeq2 4403 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑞) → 〈𝑝, 𝑦〉 = 〈𝑝, (𝐹‘𝑞)〉) |
125 | 124 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑞) → (〈𝑝, 𝑦〉 ∈ dom ∙ ↔ 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
126 | 125 | ralrn 6362 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
127 | 11, 92, 126 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
128 | 127 | ralbidv 2986 |
. . . . . . 7
⊢ (𝜑 → (∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝐾 ∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
129 | 123, 128 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ) |
130 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑥 = 〈𝑝, 𝑦〉 → (𝑥 ∈ dom ∙ ↔ 〈𝑝, 𝑦〉 ∈ dom ∙ )) |
131 | 130 | ralxp 5263 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐾 × ran 𝐹)𝑥 ∈ dom ∙ ↔
∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ) |
132 | 129, 131 | sylibr 224 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (𝐾 × ran 𝐹)𝑥 ∈ dom ∙ ) |
133 | | dfss3 3592 |
. . . . 5
⊢ ((𝐾 × ran 𝐹) ⊆ dom ∙ ↔
∀𝑥 ∈ (𝐾 × ran 𝐹)𝑥 ∈ dom ∙ ) |
134 | 132, 133 | sylibr 224 |
. . . 4
⊢ (𝜑 → (𝐾 × ran 𝐹) ⊆ dom ∙ ) |
135 | 44, 134 | eqsstr3d 3640 |
. . 3
⊢ (𝜑 → (𝐾 × 𝐵) ⊆ dom ∙ ) |
136 | 41, 135 | eqssd 3620 |
. 2
⊢ (𝜑 → dom ∙ = (𝐾 × 𝐵)) |
137 | | df-fn 5891 |
. 2
⊢ ( ∙ Fn
(𝐾 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ =
(𝐾 × 𝐵))) |
138 | 107, 136,
137 | sylanbrc 698 |
1
⊢ (𝜑 → ∙ Fn (𝐾 × 𝐵)) |