| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
| 2 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐹‘(𝑝 · 𝑞)) ∈ V |
| 3 | 1, 2 | fnmpoi 8095 |
. . . . . . 7
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹‘𝑞)}) |
| 4 | | fnrel 6670 |
. . . . . . 7
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹‘𝑞)}) → Rel (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢ Rel
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
| 6 | 5 | rgenw 3065 |
. . . . 5
⊢
∀𝑞 ∈
𝑉 Rel (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
| 7 | | reliun 5826 |
. . . . 5
⊢ (Rel
∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ↔ ∀𝑞 ∈ 𝑉 Rel (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
| 8 | 6, 7 | mpbir 231 |
. . . 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 17565 |
. . . . 5
⊢ (𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
| 18 | 17 | releqd 5788 |
. . . 4
⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))) |
| 19 | 8, 18 | mpbiri 258 |
. . 3
⊢ (𝜑 → Rel ∙ ) |
| 20 | | dffn2 6738 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹‘𝑞)}) ↔ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹‘𝑞)})⟶V) |
| 21 | 3, 20 | mpbi 230 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹‘𝑞)})⟶V |
| 22 | | fssxp 6763 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹‘𝑞)})⟶V → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × {(𝐹‘𝑞)}) × V)) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × {(𝐹‘𝑞)}) × V) |
| 24 | | fof 6820 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
| 25 | 11, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
| 26 | 25 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵) |
| 27 | 26 | snssd 4809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → {(𝐹‘𝑞)} ⊆ 𝐵) |
| 28 | | xpss2 5705 |
. . . . . . . . . . . 12
⊢ ({(𝐹‘𝑞)} ⊆ 𝐵 → (𝐾 × {(𝐹‘𝑞)}) ⊆ (𝐾 × 𝐵)) |
| 29 | | xpss1 5704 |
. . . . . . . . . . . 12
⊢ ((𝐾 × {(𝐹‘𝑞)}) ⊆ (𝐾 × 𝐵) → ((𝐾 × {(𝐹‘𝑞)}) × V) ⊆ ((𝐾 × 𝐵) × V)) |
| 30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → ((𝐾 × {(𝐹‘𝑞)}) × V) ⊆ ((𝐾 × 𝐵) × V)) |
| 31 | 23, 30 | sstrid 3995 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
| 32 | 31 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
| 33 | | iunss 5045 |
. . . . . . . . 9
⊢ (∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V) ↔ ∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
| 34 | 32, 33 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V)) |
| 35 | 17, 34 | eqsstrd 4018 |
. . . . . . 7
⊢ (𝜑 → ∙ ⊆ ((𝐾 × 𝐵) × V)) |
| 36 | | dmss 5913 |
. . . . . . 7
⊢ ( ∙
⊆ ((𝐾 × 𝐵) × V) → dom ∙
⊆ dom ((𝐾 ×
𝐵) ×
V)) |
| 37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom ∙ ⊆ dom ((𝐾 × 𝐵) × V)) |
| 38 | | vn0 4345 |
. . . . . . 7
⊢ V ≠
∅ |
| 39 | | dmxp 5939 |
. . . . . . 7
⊢ (V ≠
∅ → dom ((𝐾
× 𝐵) × V) =
(𝐾 × 𝐵)) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . 6
⊢ dom
((𝐾 × 𝐵) × V) = (𝐾 × 𝐵) |
| 41 | 37, 40 | sseqtrdi 4024 |
. . . . 5
⊢ (𝜑 → dom ∙ ⊆ (𝐾 × 𝐵)) |
| 42 | | forn 6823 |
. . . . . . 7
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) |
| 43 | 11, 42 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 = 𝐵) |
| 44 | 43 | xpeq2d 5715 |
. . . . 5
⊢ (𝜑 → (𝐾 × ran 𝐹) = (𝐾 × 𝐵)) |
| 45 | 41, 44 | sseqtrrd 4021 |
. . . 4
⊢ (𝜑 → dom ∙ ⊆ (𝐾 × ran 𝐹)) |
| 46 | | df-br 5144 |
. . . . . . . . . 10
⊢
(〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 ↔ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ ) |
| 47 | 17 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ ↔
〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ ↔
〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))) |
| 49 | | eliun 4995 |
. . . . . . . . . . . 12
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ↔ ∃𝑞 ∈ 𝑉 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
| 50 | | df-3an 1089 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉) ↔ ((𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉)) |
| 51 | 1 | mpofun 7557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Fun
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) |
| 52 | | funopfv 6958 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Fun
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) = 𝑤)) |
| 53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) = 𝑤) |
| 54 | | df-ov 7434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹‘𝑎)) = ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) |
| 55 | | opex 5469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
〈𝑝, (𝐹‘𝑎)〉 ∈ V |
| 56 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑤 ∈ V |
| 57 | 55, 56 | opeldm 5918 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 〈𝑝, (𝐹‘𝑎)〉 ∈ dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
| 58 | 1, 2 | dmmpo 8096 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝐾 × {(𝐹‘𝑞)}) |
| 59 | 57, 58 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 〈𝑝, (𝐹‘𝑎)〉 ∈ (𝐾 × {(𝐹‘𝑞)})) |
| 60 | | opelxp 5721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝑝, (𝐹‘𝑎)〉 ∈ (𝐾 × {(𝐹‘𝑞)}) ↔ (𝑝 ∈ 𝐾 ∧ (𝐹‘𝑎) ∈ {(𝐹‘𝑞)})) |
| 61 | 59, 60 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝑝 ∈ 𝐾 ∧ (𝐹‘𝑎) ∈ {(𝐹‘𝑞)})) |
| 62 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑝 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑝 · 𝑞))) |
| 63 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝐹‘𝑎) → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑝 · 𝑞))) |
| 64 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = 𝑧 → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑧 · 𝑞))) |
| 65 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑧 · 𝑞))) |
| 66 | 64, 65 | cbvmpov 7528 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝑧 ∈ 𝐾, 𝑦 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑧 · 𝑞))) |
| 67 | 62, 63, 66, 2 | ovmpo 7593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ 𝐾 ∧ (𝐹‘𝑎) ∈ {(𝐹‘𝑞)}) → (𝑝(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹‘𝑎)) = (𝐹‘(𝑝 · 𝑞))) |
| 68 | 61, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝑝(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹‘𝑎)) = (𝐹‘(𝑝 · 𝑞))) |
| 69 | 54, 68 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘〈𝑝, (𝐹‘𝑎)〉) = (𝐹‘(𝑝 · 𝑞))) |
| 70 | 53, 69 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑞))) |
| 71 | 70 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) ∧ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → 𝑤 = (𝐹‘(𝑝 · 𝑞))) |
| 72 | | imasvscaf.e |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))) |
| 73 | | elsni 4643 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑎) ∈ {(𝐹‘𝑞)} → (𝐹‘𝑎) = (𝐹‘𝑞)) |
| 74 | 61, 73 | simpl2im 503 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑝,
(𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝐹‘𝑎) = (𝐹‘𝑞)) |
| 75 | 72, 74 | impel 505 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) ∧ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))) |
| 76 | 71, 75 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) ∧ 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → 𝑤 = (𝐹‘(𝑝 · 𝑎))) |
| 77 | 76 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 78 | 50, 77 | sylan2br 595 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 79 | 78 | anassrs 467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑞 ∈ 𝑉) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 80 | 79 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (∃𝑞 ∈ 𝑉 〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 81 | 49, 80 | biimtrid 242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 82 | 48, 81 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈〈𝑝, (𝐹‘𝑎)〉, 𝑤〉 ∈ ∙ → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 83 | 46, 82 | biimtrid 242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → (〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 84 | 83 | alrimiv 1927 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → ∀𝑤(〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑝 · 𝑎)))) |
| 85 | | mo2icl 3720 |
. . . . . . . 8
⊢
(∀𝑤(〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑝 · 𝑎))) → ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤) |
| 86 | 84, 85 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉)) → ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤) |
| 87 | 86 | ralrimivva 3202 |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤) |
| 88 | | fofn 6822 |
. . . . . . . 8
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉) |
| 89 | | opeq2 4874 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑎) → 〈𝑝, 𝑦〉 = 〈𝑝, (𝐹‘𝑎)〉) |
| 90 | 89 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑎) → (〈𝑝, 𝑦〉 ∙ 𝑤 ↔ 〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
| 91 | 90 | mobidv 2549 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑎) → (∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
| 92 | 91 | ralrn 7108 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
| 93 | 11, 88, 92 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
| 94 | 93 | ralbidv 3178 |
. . . . . 6
⊢ (𝜑 → (∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤 ↔ ∀𝑝 ∈ 𝐾 ∀𝑎 ∈ 𝑉 ∃*𝑤〈𝑝, (𝐹‘𝑎)〉 ∙ 𝑤)) |
| 95 | 87, 94 | mpbird 257 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤) |
| 96 | | breq1 5146 |
. . . . . . 7
⊢ (𝑥 = 〈𝑝, 𝑦〉 → (𝑥 ∙ 𝑤 ↔ 〈𝑝, 𝑦〉 ∙ 𝑤)) |
| 97 | 96 | mobidv 2549 |
. . . . . 6
⊢ (𝑥 = 〈𝑝, 𝑦〉 → (∃*𝑤 𝑥 ∙ 𝑤 ↔ ∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤)) |
| 98 | 97 | ralxp 5852 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐾 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹∃*𝑤〈𝑝, 𝑦〉 ∙ 𝑤) |
| 99 | 95, 98 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐾 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤) |
| 100 | | ssralv 4052 |
. . . 4
⊢ (dom
∙
⊆ (𝐾 × ran
𝐹) → (∀𝑥 ∈ (𝐾 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
| 101 | 45, 99, 100 | sylc 65 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤) |
| 102 | | dffun7 6593 |
. . 3
⊢ (Fun
∙
↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
| 103 | 19, 101, 102 | sylanbrc 583 |
. 2
⊢ (𝜑 → Fun ∙ ) |
| 104 | | eqimss2 4043 |
. . . . . . . . . . . . . . 15
⊢ ( ∙ =
∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
| 105 | 17, 104 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
| 106 | | iunss 5045 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ↔
∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
| 107 | 105, 106 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
| 108 | 107 | r19.21bi 3251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝑉) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
| 109 | 108 | adantrl 716 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ ) |
| 110 | | dmss 5913 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ∙ → dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ dom ∙ ) |
| 111 | 109, 110 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ dom ∙ ) |
| 112 | 58, 111 | eqsstrrid 4023 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → (𝐾 × {(𝐹‘𝑞)}) ⊆ dom ∙ ) |
| 113 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → 𝑝 ∈ 𝐾) |
| 114 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑞) ∈ V |
| 115 | 114 | snid 4662 |
. . . . . . . . . 10
⊢ (𝐹‘𝑞) ∈ {(𝐹‘𝑞)} |
| 116 | | opelxpi 5722 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ 𝐾 ∧ (𝐹‘𝑞) ∈ {(𝐹‘𝑞)}) → 〈𝑝, (𝐹‘𝑞)〉 ∈ (𝐾 × {(𝐹‘𝑞)})) |
| 117 | 113, 115,
116 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → 〈𝑝, (𝐹‘𝑞)〉 ∈ (𝐾 × {(𝐹‘𝑞)})) |
| 118 | 112, 117 | sseldd 3984 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ ) |
| 119 | 118 | ralrimivva 3202 |
. . . . . . 7
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ ) |
| 120 | | opeq2 4874 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑞) → 〈𝑝, 𝑦〉 = 〈𝑝, (𝐹‘𝑞)〉) |
| 121 | 120 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑞) → (〈𝑝, 𝑦〉 ∈ dom ∙ ↔ 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
| 122 | 121 | ralrn 7108 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
| 123 | 11, 88, 122 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
| 124 | 123 | ralbidv 3178 |
. . . . . . 7
⊢ (𝜑 → (∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝐾 ∀𝑞 ∈ 𝑉 〈𝑝, (𝐹‘𝑞)〉 ∈ dom ∙ )) |
| 125 | 119, 124 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ) |
| 126 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑥 = 〈𝑝, 𝑦〉 → (𝑥 ∈ dom ∙ ↔ 〈𝑝, 𝑦〉 ∈ dom ∙ )) |
| 127 | 126 | ralxp 5852 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐾 × ran 𝐹)𝑥 ∈ dom ∙ ↔
∀𝑝 ∈ 𝐾 ∀𝑦 ∈ ran 𝐹〈𝑝, 𝑦〉 ∈ dom ∙ ) |
| 128 | 125, 127 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (𝐾 × ran 𝐹)𝑥 ∈ dom ∙ ) |
| 129 | | dfss3 3972 |
. . . . 5
⊢ ((𝐾 × ran 𝐹) ⊆ dom ∙ ↔
∀𝑥 ∈ (𝐾 × ran 𝐹)𝑥 ∈ dom ∙ ) |
| 130 | 128, 129 | sylibr 234 |
. . . 4
⊢ (𝜑 → (𝐾 × ran 𝐹) ⊆ dom ∙ ) |
| 131 | 44, 130 | eqsstrrd 4019 |
. . 3
⊢ (𝜑 → (𝐾 × 𝐵) ⊆ dom ∙ ) |
| 132 | 41, 131 | eqssd 4001 |
. 2
⊢ (𝜑 → dom ∙ = (𝐾 × 𝐵)) |
| 133 | | df-fn 6564 |
. 2
⊢ ( ∙ Fn
(𝐾 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ =
(𝐾 × 𝐵))) |
| 134 | 103, 132,
133 | sylanbrc 583 |
1
⊢ (𝜑 → ∙ Fn (𝐾 × 𝐵)) |