Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imasvscafn Structured version   Visualization version   GIF version

Theorem imasvscafn 16020
 Description: The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
imasvscaf.u (𝜑𝑈 = (𝐹s 𝑅))
imasvscaf.v (𝜑𝑉 = (Base‘𝑅))
imasvscaf.f (𝜑𝐹:𝑉onto𝐵)
imasvscaf.r (𝜑𝑅𝑍)
imasvscaf.g 𝐺 = (Scalar‘𝑅)
imasvscaf.k 𝐾 = (Base‘𝐺)
imasvscaf.q · = ( ·𝑠𝑅)
imasvscaf.s = ( ·𝑠𝑈)
imasvscaf.e ((𝜑 ∧ (𝑝𝐾𝑎𝑉𝑞𝑉)) → ((𝐹𝑎) = (𝐹𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))
Assertion
Ref Expression
imasvscafn (𝜑 Fn (𝐾 × 𝐵))
Distinct variable groups:   𝑝,𝑎,𝑞,𝐹   𝐾,𝑎,𝑝,𝑞   𝜑,𝑎,𝑝,𝑞   𝐵,𝑝,𝑞   𝑅,𝑝,𝑞   · ,𝑝,𝑞   ,𝑎,𝑝,𝑞   𝑉,𝑎,𝑝,𝑞
Allowed substitution hints:   𝐵(𝑎)   𝑅(𝑎)   · (𝑎)   𝑈(𝑞,𝑝,𝑎)   𝐺(𝑞,𝑝,𝑎)   𝑍(𝑞,𝑝,𝑎)

Proof of Theorem imasvscafn
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2610 . . . . . . . 8 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))
2 fvex 6113 . . . . . . . 8 (𝐹‘(𝑝 · 𝑞)) ∈ V
31, 2fnmpt2i 7128 . . . . . . 7 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹𝑞)})
4 fnrel 5903 . . . . . . 7 ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹𝑞)}) → Rel (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
53, 4ax-mp 5 . . . . . 6 Rel (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))
65rgenw 2908 . . . . 5 𝑞𝑉 Rel (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))
7 reliun 5162 . . . . 5 (Rel 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ↔ ∀𝑞𝑉 Rel (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
86, 7mpbir 220 . . . 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 = ( ·𝑠𝑈)
179, 10, 11, 12, 13, 14, 15, 16imasvsca 16003 . . . . 5 (𝜑 = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
1817releqd 5126 . . . 4 (𝜑 → (Rel ↔ Rel 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))))
198, 18mpbiri 247 . . 3 (𝜑 → Rel )
20 dffn2 5960 . . . . . . . . . . . . 13 ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) Fn (𝐾 × {(𝐹𝑞)}) ↔ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹𝑞)})⟶V)
213, 20mpbi 219 . . . . . . . . . . . 12 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹𝑞)})⟶V
22 fssxp 5973 . . . . . . . . . . . 12 ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))):(𝐾 × {(𝐹𝑞)})⟶V → (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × {(𝐹𝑞)}) × V))
2321, 22ax-mp 5 . . . . . . . . . . 11 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × {(𝐹𝑞)}) × V)
24 fof 6028 . . . . . . . . . . . . . . 15 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
2511, 24syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹:𝑉𝐵)
2625ffvelrnda 6267 . . . . . . . . . . . . 13 ((𝜑𝑞𝑉) → (𝐹𝑞) ∈ 𝐵)
2726snssd 4281 . . . . . . . . . . . 12 ((𝜑𝑞𝑉) → {(𝐹𝑞)} ⊆ 𝐵)
28 xpss2 5152 . . . . . . . . . . . 12 ({(𝐹𝑞)} ⊆ 𝐵 → (𝐾 × {(𝐹𝑞)}) ⊆ (𝐾 × 𝐵))
29 xpss1 5151 . . . . . . . . . . . 12 ((𝐾 × {(𝐹𝑞)}) ⊆ (𝐾 × 𝐵) → ((𝐾 × {(𝐹𝑞)}) × V) ⊆ ((𝐾 × 𝐵) × V))
3027, 28, 293syl 18 . . . . . . . . . . 11 ((𝜑𝑞𝑉) → ((𝐾 × {(𝐹𝑞)}) × V) ⊆ ((𝐾 × 𝐵) × V))
3123, 30syl5ss 3579 . . . . . . . . . 10 ((𝜑𝑞𝑉) → (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V))
3231ralrimiva 2949 . . . . . . . . 9 (𝜑 → ∀𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V))
33 iunss 4497 . . . . . . . . 9 ( 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V) ↔ ∀𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V))
3432, 33sylibr 223 . . . . . . . 8 (𝜑 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ((𝐾 × 𝐵) × V))
3517, 34eqsstrd 3602 . . . . . . 7 (𝜑 ⊆ ((𝐾 × 𝐵) × V))
36 dmss 5245 . . . . . . 7 ( ⊆ ((𝐾 × 𝐵) × V) → dom ⊆ dom ((𝐾 × 𝐵) × V))
3735, 36syl 17 . . . . . 6 (𝜑 → dom ⊆ dom ((𝐾 × 𝐵) × V))
38 vn0 3883 . . . . . . 7 V ≠ ∅
39 dmxp 5265 . . . . . . 7 (V ≠ ∅ → dom ((𝐾 × 𝐵) × V) = (𝐾 × 𝐵))
4038, 39ax-mp 5 . . . . . 6 dom ((𝐾 × 𝐵) × V) = (𝐾 × 𝐵)
4137, 40syl6sseq 3614 . . . . 5 (𝜑 → dom ⊆ (𝐾 × 𝐵))
42 forn 6031 . . . . . . 7 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
4311, 42syl 17 . . . . . 6 (𝜑 → ran 𝐹 = 𝐵)
4443xpeq2d 5063 . . . . 5 (𝜑 → (𝐾 × ran 𝐹) = (𝐾 × 𝐵))
4541, 44sseqtr4d 3605 . . . 4 (𝜑 → dom ⊆ (𝐾 × ran 𝐹))
46 df-br 4584 . . . . . . . . . 10 (⟨𝑝, (𝐹𝑎)⟩ 𝑤 ↔ ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ )
4717eleq2d 2673 . . . . . . . . . . . 12 (𝜑 → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ ↔ ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))))
4847adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐾𝑎𝑉)) → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ ↔ ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))))
49 eliun 4460 . . . . . . . . . . . 12 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ↔ ∃𝑞𝑉 ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
50 df-3an 1033 . . . . . . . . . . . . . . 15 ((𝑝𝐾𝑎𝑉𝑞𝑉) ↔ ((𝑝𝐾𝑎𝑉) ∧ 𝑞𝑉))
511mpt2fun 6660 . . . . . . . . . . . . . . . . . . . 20 Fun (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))
52 funopfv 6145 . . . . . . . . . . . . . . . . . . . 20 (Fun (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘⟨𝑝, (𝐹𝑎)⟩) = 𝑤))
5351, 52ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘⟨𝑝, (𝐹𝑎)⟩) = 𝑤)
54 df-ov 6552 . . . . . . . . . . . . . . . . . . . 20 (𝑝(𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹𝑎)) = ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘⟨𝑝, (𝐹𝑎)⟩)
55 opex 4859 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑝, (𝐹𝑎)⟩ ∈ V
56 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
5755, 56opeldm 5250 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ⟨𝑝, (𝐹𝑎)⟩ ∈ dom (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
581, 2dmmpt2 7129 . . . . . . . . . . . . . . . . . . . . . . 23 dom (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝐾 × {(𝐹𝑞)})
5957, 58syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . 22 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ⟨𝑝, (𝐹𝑎)⟩ ∈ (𝐾 × {(𝐹𝑞)}))
60 opelxp 5070 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑝, (𝐹𝑎)⟩ ∈ (𝐾 × {(𝐹𝑞)}) ↔ (𝑝𝐾 ∧ (𝐹𝑎) ∈ {(𝐹𝑞)}))
6159, 60sylib 207 . . . . . . . . . . . . . . . . . . . . 21 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝑝𝐾 ∧ (𝐹𝑎) ∈ {(𝐹𝑞)}))
62 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑝 → (𝑧 · 𝑞) = (𝑝 · 𝑞))
6362fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑝 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑝 · 𝑞)))
64 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝐹𝑎) → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑝 · 𝑞)))
6563equcoms 1934 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑧 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑝 · 𝑞)))
6665eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑧 → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑧 · 𝑞)))
67 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝐹‘(𝑧 · 𝑞)) = (𝐹‘(𝑧 · 𝑞)))
6866, 67cbvmpt2v 6633 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝑧𝐾, 𝑦 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑧 · 𝑞)))
6963, 64, 68, 2ovmpt2 6694 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝𝐾 ∧ (𝐹𝑎) ∈ {(𝐹𝑞)}) → (𝑝(𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹𝑎)) = (𝐹‘(𝑝 · 𝑞)))
7061, 69syl 17 . . . . . . . . . . . . . . . . . . . 20 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝑝(𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))(𝐹𝑎)) = (𝐹‘(𝑝 · 𝑞)))
7154, 70syl5eqr 2658 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))‘⟨𝑝, (𝐹𝑎)⟩) = (𝐹‘(𝑝 · 𝑞)))
7253, 71eqtr3d 2646 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑞)))
7372adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑝𝐾𝑎𝑉𝑞𝑉)) ∧ ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → 𝑤 = (𝐹‘(𝑝 · 𝑞)))
7461simprd 478 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝐹𝑎) ∈ {(𝐹𝑞)})
75 elsni 4142 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑎) ∈ {(𝐹𝑞)} → (𝐹𝑎) = (𝐹𝑞))
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → (𝐹𝑎) = (𝐹𝑞))
77 imasvscaf.e . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐾𝑎𝑉𝑞𝑉)) → ((𝐹𝑎) = (𝐹𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))
7877imp 444 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑝𝐾𝑎𝑉𝑞𝑉)) ∧ (𝐹𝑎) = (𝐹𝑞)) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))
7976, 78sylan2 490 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑝𝐾𝑎𝑉𝑞𝑉)) ∧ ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))
8073, 79eqtr4d 2647 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑝𝐾𝑎𝑉𝑞𝑉)) ∧ ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) → 𝑤 = (𝐹‘(𝑝 · 𝑎)))
8180ex 449 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐾𝑎𝑉𝑞𝑉)) → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎))))
8250, 81sylan2br 492 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑝𝐾𝑎𝑉) ∧ 𝑞𝑉)) → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎))))
8382anassrs 678 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐾𝑎𝑉)) ∧ 𝑞𝑉) → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎))))
8483rexlimdva 3013 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝐾𝑎𝑉)) → (∃𝑞𝑉 ⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎))))
8549, 84syl5bi 231 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐾𝑎𝑉)) → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑝 · 𝑎))))
8648, 85sylbid 229 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐾𝑎𝑉)) → (⟨⟨𝑝, (𝐹𝑎)⟩, 𝑤⟩ ∈ 𝑤 = (𝐹‘(𝑝 · 𝑎))))
8746, 86syl5bi 231 . . . . . . . . 9 ((𝜑 ∧ (𝑝𝐾𝑎𝑉)) → (⟨𝑝, (𝐹𝑎)⟩ 𝑤𝑤 = (𝐹‘(𝑝 · 𝑎))))
8887alrimiv 1842 . . . . . . . 8 ((𝜑 ∧ (𝑝𝐾𝑎𝑉)) → ∀𝑤(⟨𝑝, (𝐹𝑎)⟩ 𝑤𝑤 = (𝐹‘(𝑝 · 𝑎))))
89 mo2icl 3352 . . . . . . . 8 (∀𝑤(⟨𝑝, (𝐹𝑎)⟩ 𝑤𝑤 = (𝐹‘(𝑝 · 𝑎))) → ∃*𝑤𝑝, (𝐹𝑎)⟩ 𝑤)
9088, 89syl 17 . . . . . . 7 ((𝜑 ∧ (𝑝𝐾𝑎𝑉)) → ∃*𝑤𝑝, (𝐹𝑎)⟩ 𝑤)
9190ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑝𝐾𝑎𝑉 ∃*𝑤𝑝, (𝐹𝑎)⟩ 𝑤)
92 fofn 6030 . . . . . . . 8 (𝐹:𝑉onto𝐵𝐹 Fn 𝑉)
93 opeq2 4341 . . . . . . . . . . 11 (𝑦 = (𝐹𝑎) → ⟨𝑝, 𝑦⟩ = ⟨𝑝, (𝐹𝑎)⟩)
9493breq1d 4593 . . . . . . . . . 10 (𝑦 = (𝐹𝑎) → (⟨𝑝, 𝑦 𝑤 ↔ ⟨𝑝, (𝐹𝑎)⟩ 𝑤))
9594mobidv 2479 . . . . . . . . 9 (𝑦 = (𝐹𝑎) → (∃*𝑤𝑝, 𝑦 𝑤 ↔ ∃*𝑤𝑝, (𝐹𝑎)⟩ 𝑤))
9695ralrn 6270 . . . . . . . 8 (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∃*𝑤𝑝, 𝑦 𝑤 ↔ ∀𝑎𝑉 ∃*𝑤𝑝, (𝐹𝑎)⟩ 𝑤))
9711, 92, 963syl 18 . . . . . . 7 (𝜑 → (∀𝑦 ∈ ran 𝐹∃*𝑤𝑝, 𝑦 𝑤 ↔ ∀𝑎𝑉 ∃*𝑤𝑝, (𝐹𝑎)⟩ 𝑤))
9897ralbidv 2969 . . . . . 6 (𝜑 → (∀𝑝𝐾𝑦 ∈ ran 𝐹∃*𝑤𝑝, 𝑦 𝑤 ↔ ∀𝑝𝐾𝑎𝑉 ∃*𝑤𝑝, (𝐹𝑎)⟩ 𝑤))
9991, 98mpbird 246 . . . . 5 (𝜑 → ∀𝑝𝐾𝑦 ∈ ran 𝐹∃*𝑤𝑝, 𝑦 𝑤)
100 breq1 4586 . . . . . . 7 (𝑥 = ⟨𝑝, 𝑦⟩ → (𝑥 𝑤 ↔ ⟨𝑝, 𝑦 𝑤))
101100mobidv 2479 . . . . . 6 (𝑥 = ⟨𝑝, 𝑦⟩ → (∃*𝑤 𝑥 𝑤 ↔ ∃*𝑤𝑝, 𝑦 𝑤))
102101ralxp 5185 . . . . 5 (∀𝑥 ∈ (𝐾 × ran 𝐹)∃*𝑤 𝑥 𝑤 ↔ ∀𝑝𝐾𝑦 ∈ ran 𝐹∃*𝑤𝑝, 𝑦 𝑤)
10399, 102sylibr 223 . . . 4 (𝜑 → ∀𝑥 ∈ (𝐾 × ran 𝐹)∃*𝑤 𝑥 𝑤)
104 ssralv 3629 . . . 4 (dom ⊆ (𝐾 × ran 𝐹) → (∀𝑥 ∈ (𝐾 × ran 𝐹)∃*𝑤 𝑥 𝑤 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
10545, 103, 104sylc 63 . . 3 (𝜑 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤)
106 dffun7 5830 . . 3 (Fun ↔ (Rel ∧ ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
10719, 105, 106sylanbrc 695 . 2 (𝜑 → Fun )
108 eqimss2 3621 . . . . . . . . . . . . . . 15 ( = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) → 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ )
10917, 108syl 17 . . . . . . . . . . . . . 14 (𝜑 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ )
110 iunss 4497 . . . . . . . . . . . . . 14 ( 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ ↔ ∀𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ )
111109, 110sylib 207 . . . . . . . . . . . . 13 (𝜑 → ∀𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ )
112111r19.21bi 2916 . . . . . . . . . . . 12 ((𝜑𝑞𝑉) → (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ )
113112adantrl 748 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐾𝑞𝑉)) → (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ )
114 dmss 5245 . . . . . . . . . . 11 ((𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ → dom (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ dom )
115113, 114syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐾𝑞𝑉)) → dom (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) ⊆ dom )
11658, 115syl5eqssr 3613 . . . . . . . . 9 ((𝜑 ∧ (𝑝𝐾𝑞𝑉)) → (𝐾 × {(𝐹𝑞)}) ⊆ dom )
117 simprl 790 . . . . . . . . . 10 ((𝜑 ∧ (𝑝𝐾𝑞𝑉)) → 𝑝𝐾)
118 fvex 6113 . . . . . . . . . . 11 (𝐹𝑞) ∈ V
119118snid 4155 . . . . . . . . . 10 (𝐹𝑞) ∈ {(𝐹𝑞)}
120 opelxpi 5072 . . . . . . . . . 10 ((𝑝𝐾 ∧ (𝐹𝑞) ∈ {(𝐹𝑞)}) → ⟨𝑝, (𝐹𝑞)⟩ ∈ (𝐾 × {(𝐹𝑞)}))
121117, 119, 120sylancl 693 . . . . . . . . 9 ((𝜑 ∧ (𝑝𝐾𝑞𝑉)) → ⟨𝑝, (𝐹𝑞)⟩ ∈ (𝐾 × {(𝐹𝑞)}))
122116, 121sseldd 3569 . . . . . . . 8 ((𝜑 ∧ (𝑝𝐾𝑞𝑉)) → ⟨𝑝, (𝐹𝑞)⟩ ∈ dom )
123122ralrimivva 2954 . . . . . . 7 (𝜑 → ∀𝑝𝐾𝑞𝑉𝑝, (𝐹𝑞)⟩ ∈ dom )
124 opeq2 4341 . . . . . . . . . . 11 (𝑦 = (𝐹𝑞) → ⟨𝑝, 𝑦⟩ = ⟨𝑝, (𝐹𝑞)⟩)
125124eleq1d 2672 . . . . . . . . . 10 (𝑦 = (𝐹𝑞) → (⟨𝑝, 𝑦⟩ ∈ dom ↔ ⟨𝑝, (𝐹𝑞)⟩ ∈ dom ))
126125ralrn 6270 . . . . . . . . 9 (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹𝑝, 𝑦⟩ ∈ dom ↔ ∀𝑞𝑉𝑝, (𝐹𝑞)⟩ ∈ dom ))
12711, 92, 1263syl 18 . . . . . . . 8 (𝜑 → (∀𝑦 ∈ ran 𝐹𝑝, 𝑦⟩ ∈ dom ↔ ∀𝑞𝑉𝑝, (𝐹𝑞)⟩ ∈ dom ))
128127ralbidv 2969 . . . . . . 7 (𝜑 → (∀𝑝𝐾𝑦 ∈ ran 𝐹𝑝, 𝑦⟩ ∈ dom ↔ ∀𝑝𝐾𝑞𝑉𝑝, (𝐹𝑞)⟩ ∈ dom ))
129123, 128mpbird 246 . . . . . 6 (𝜑 → ∀𝑝𝐾𝑦 ∈ ran 𝐹𝑝, 𝑦⟩ ∈ dom )
130 eleq1 2676 . . . . . . 7 (𝑥 = ⟨𝑝, 𝑦⟩ → (𝑥 ∈ dom ↔ ⟨𝑝, 𝑦⟩ ∈ dom ))
131130ralxp 5185 . . . . . 6 (∀𝑥 ∈ (𝐾 × ran 𝐹)𝑥 ∈ dom ↔ ∀𝑝𝐾𝑦 ∈ ran 𝐹𝑝, 𝑦⟩ ∈ dom )
132129, 131sylibr 223 . . . . 5 (𝜑 → ∀𝑥 ∈ (𝐾 × ran 𝐹)𝑥 ∈ dom )
133 dfss3 3558 . . . . 5 ((𝐾 × ran 𝐹) ⊆ dom ↔ ∀𝑥 ∈ (𝐾 × ran 𝐹)𝑥 ∈ dom )
134132, 133sylibr 223 . . . 4 (𝜑 → (𝐾 × ran 𝐹) ⊆ dom )
13544, 134eqsstr3d 3603 . . 3 (𝜑 → (𝐾 × 𝐵) ⊆ dom )
13641, 135eqssd 3585 . 2 (𝜑 → dom = (𝐾 × 𝐵))
137 df-fn 5807 . 2 ( Fn (𝐾 × 𝐵) ↔ (Fun ∧ dom = (𝐾 × 𝐵)))
138107, 136, 137sylanbrc 695 1 (𝜑 Fn (𝐾 × 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475   ∈ wcel 1977  ∃*wmo 2459   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  {csn 4125  ⟨cop 4131  ∪ ciun 4455   class class class wbr 4583   × cxp 5036  dom cdm 5038  ran crn 5039  Rel wrel 5043  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  Basecbs 15695  Scalarcsca 15771   ·𝑠 cvsca 15772   “s cimas 15987 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-imas 15991 This theorem is referenced by:  imasvscaval  16021  imasvscaf  16022
 Copyright terms: Public domain W3C validator