Step | Hyp | Ref
| Expression |
1 | | ismid.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
2 | | ismid.d |
. . . . 5
⊢ − =
(dist‘𝐺) |
3 | | ismid.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
4 | | ismid.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝐺 ∈ TarskiG) |
6 | | ismid.1 |
. . . . . 6
⊢ (𝜑 → 𝐺DimTarskiG≥2) |
7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝐺DimTarskiG≥2) |
8 | | lmif.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
9 | | lmif.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝐷 ∈ ran 𝐿) |
11 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝑎 ∈ 𝑃) |
12 | 1, 2, 3, 5, 7, 8, 10, 11 | lmieu 25476 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ∃!𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) |
13 | | riotacl 6525 |
. . . 4
⊢
(∃!𝑏 ∈
𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)) → (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) ∈ 𝑃) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) ∈ 𝑃) |
15 | | eqid 2610 |
. . 3
⊢ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
16 | 14, 15 | fmptd 6292 |
. 2
⊢ (𝜑 → (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))):𝑃⟶𝑃) |
17 | | lmif.m |
. . . 4
⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) |
18 | | df-lmi 25467 |
. . . . . . 7
⊢ lInvG =
(𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))) |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (𝜑 → lInvG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))) |
20 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = (LineG‘𝐺)) |
21 | 20, 8 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = 𝐿) |
22 | 21 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ran (LineG‘𝑔) = ran 𝐿) |
23 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
24 | 23, 1 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
25 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (midG‘𝑔) = (midG‘𝐺)) |
26 | 25 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (𝑎(midG‘𝑔)𝑏) = (𝑎(midG‘𝐺)𝑏)) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ↔ (𝑎(midG‘𝐺)𝑏) ∈ 𝑑)) |
28 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → 𝑑 = 𝑑) |
29 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (⟂G‘𝑔) = (⟂G‘𝐺)) |
30 | 21 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (𝑎(LineG‘𝑔)𝑏) = (𝑎𝐿𝑏)) |
31 | 28, 29, 30 | breq123d 4597 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ↔ 𝑑(⟂G‘𝐺)(𝑎𝐿𝑏))) |
32 | 31 | orbi1d 735 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏) ↔ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) |
33 | 27, 32 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)) ↔ ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
34 | 24, 33 | riotaeqbidv 6514 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))) = (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
35 | 24, 34 | mpteq12dv 4663 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
36 | 22, 35 | mpteq12dv 4663 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑑 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))) = (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))))) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑑 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))) = (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))))) |
38 | | elex 3185 |
. . . . . . 7
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
39 | 4, 38 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
40 | | fvex 6113 |
. . . . . . . . 9
⊢
(LineG‘𝐺)
∈ V |
41 | 8, 40 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐿 ∈ V |
42 | | rnexg 6990 |
. . . . . . . 8
⊢ (𝐿 ∈ V → ran 𝐿 ∈ V) |
43 | | mptexg 6389 |
. . . . . . . 8
⊢ (ran
𝐿 ∈ V → (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) ∈ V) |
44 | 41, 42, 43 | mp2b 10 |
. . . . . . 7
⊢ (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) ∈ V |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) ∈ V) |
46 | 19, 37, 39, 45 | fvmptd 6197 |
. . . . 5
⊢ (𝜑 → (lInvG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))))) |
47 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ↔ (𝑎(midG‘𝐺)𝑏) ∈ 𝐷)) |
48 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ↔ 𝐷(⟂G‘𝐺)(𝑎𝐿𝑏))) |
49 | 48 | orbi1d 735 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → ((𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) |
50 | 47, 49 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)) ↔ ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
51 | 50 | riotabidv 6513 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) = (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
52 | 51 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑑 = 𝐷 → (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
53 | 52 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 = 𝐷) → (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
54 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝐺)
∈ V |
55 | 1, 54 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑃 ∈ V |
56 | 55 | mptex 6390 |
. . . . . 6
⊢ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) ∈ V |
57 | 56 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) ∈ V) |
58 | 46, 53, 9, 57 | fvmptd 6197 |
. . . 4
⊢ (𝜑 → ((lInvG‘𝐺)‘𝐷) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
59 | 17, 58 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
60 | 59 | feq1d 5943 |
. 2
⊢ (𝜑 → (𝑀:𝑃⟶𝑃 ↔ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))):𝑃⟶𝑃)) |
61 | 16, 60 | mpbird 246 |
1
⊢ (𝜑 → 𝑀:𝑃⟶𝑃) |