Step |
Hyp |
Ref |
Expression |
1 |
|
ismid.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
ismid.d |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
ismid.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
ismid.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
5 |
|
ismid.1 |
⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 ) |
6 |
|
lmif.m |
⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 ) |
7 |
|
lmif.l |
⊢ 𝐿 = ( LineG ‘ 𝐺 ) |
8 |
|
lmif.d |
⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 ) |
9 |
|
lmicl.1 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) |
10 |
|
islmib.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) |
11 |
|
df-lmi |
⊢ lInvG = ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ) |
12 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) ) |
13 |
12 7
|
eqtr4di |
⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = 𝐿 ) |
14 |
13
|
rneqd |
⊢ ( 𝑔 = 𝐺 → ran ( LineG ‘ 𝑔 ) = ran 𝐿 ) |
15 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) ) |
16 |
15 1
|
eqtr4di |
⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 ) |
17 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( midG ‘ 𝑔 ) = ( midG ‘ 𝐺 ) ) |
18 |
17
|
oveqd |
⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) = ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ) |
19 |
18
|
eleq1d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ↔ ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ) ) |
20 |
|
eqidd |
⊢ ( 𝑔 = 𝐺 → 𝑑 = 𝑑 ) |
21 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( ⟂G ‘ 𝑔 ) = ( ⟂G ‘ 𝐺 ) ) |
22 |
13
|
oveqd |
⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) = ( 𝑎 𝐿 𝑏 ) ) |
23 |
20 21 22
|
breq123d |
⊢ ( 𝑔 = 𝐺 → ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ↔ 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ) ) |
24 |
23
|
orbi1d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) |
25 |
19 24
|
anbi12d |
⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ↔ ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) |
26 |
16 25
|
riotaeqbidv |
⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) |
27 |
16 26
|
mpteq12dv |
⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) |
28 |
14 27
|
mpteq12dv |
⊢ ( 𝑔 = 𝐺 → ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) = ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ) |
29 |
4
|
elexd |
⊢ ( 𝜑 → 𝐺 ∈ V ) |
30 |
7
|
fvexi |
⊢ 𝐿 ∈ V |
31 |
|
rnexg |
⊢ ( 𝐿 ∈ V → ran 𝐿 ∈ V ) |
32 |
|
mptexg |
⊢ ( ran 𝐿 ∈ V → ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ∈ V ) |
33 |
30 31 32
|
mp2b |
⊢ ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ∈ V |
34 |
33
|
a1i |
⊢ ( 𝜑 → ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ∈ V ) |
35 |
11 28 29 34
|
fvmptd3 |
⊢ ( 𝜑 → ( lInvG ‘ 𝐺 ) = ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ) |
36 |
|
eleq2 |
⊢ ( 𝑑 = 𝐷 → ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ↔ ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ) |
37 |
|
breq1 |
⊢ ( 𝑑 = 𝐷 → ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ↔ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ) ) |
38 |
37
|
orbi1d |
⊢ ( 𝑑 = 𝐷 → ( ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) |
39 |
36 38
|
anbi12d |
⊢ ( 𝑑 = 𝐷 → ( ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ↔ ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) |
40 |
39
|
riotabidv |
⊢ ( 𝑑 = 𝐷 → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) |
41 |
40
|
mpteq2dv |
⊢ ( 𝑑 = 𝐷 → ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) |
42 |
41
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) |
43 |
1
|
fvexi |
⊢ 𝑃 ∈ V |
44 |
43
|
mptex |
⊢ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ∈ V |
45 |
44
|
a1i |
⊢ ( 𝜑 → ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ∈ V ) |
46 |
35 42 8 45
|
fvmptd |
⊢ ( 𝜑 → ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) |
47 |
6 46
|
syl5eq |
⊢ ( 𝜑 → 𝑀 = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) |
48 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) |
49 |
48
|
eleq1d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ) |
50 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 𝐿 𝑏 ) = ( 𝐴 𝐿 𝑏 ) ) |
51 |
50
|
breq2d |
⊢ ( 𝑎 = 𝐴 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ↔ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) ) |
52 |
|
eqeq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 = 𝑏 ↔ 𝐴 = 𝑏 ) ) |
53 |
51 52
|
orbi12d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
54 |
49 53
|
anbi12d |
⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ) |
55 |
54
|
riotabidv |
⊢ ( 𝑎 = 𝐴 → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ) |
56 |
55
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ) |
57 |
1 2 3 4 5 7 8 9
|
lmieu |
⊢ ( 𝜑 → ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
58 |
|
riotacl |
⊢ ( ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ∈ 𝑃 ) |
59 |
57 58
|
syl |
⊢ ( 𝜑 → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ∈ 𝑃 ) |
60 |
47 56 9 59
|
fvmptd |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ) |
61 |
60
|
eqeq2d |
⊢ ( 𝜑 → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ↔ 𝐵 = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ) ) |
62 |
|
oveq2 |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) |
63 |
62
|
eleq1d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ) ) |
64 |
|
oveq2 |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 𝐿 𝑏 ) = ( 𝐴 𝐿 𝐵 ) ) |
65 |
64
|
breq2d |
⊢ ( 𝑏 = 𝐵 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ↔ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ) |
66 |
|
eqeq2 |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 = 𝑏 ↔ 𝐴 = 𝐵 ) ) |
67 |
65 66
|
orbi12d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ↔ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ) |
68 |
63 67
|
anbi12d |
⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ) ) |
69 |
68
|
riota2 |
⊢ ( ( 𝐵 ∈ 𝑃 ∧ ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ↔ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) = 𝐵 ) ) |
70 |
10 57 69
|
syl2anc |
⊢ ( 𝜑 → ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ↔ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) = 𝐵 ) ) |
71 |
|
eqcom |
⊢ ( 𝐵 = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ↔ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) = 𝐵 ) |
72 |
70 71
|
bitr4di |
⊢ ( 𝜑 → ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ↔ 𝐵 = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) ) ) |
73 |
61 72
|
bitr4d |
⊢ ( 𝜑 → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ) ) |