Metamath Proof Explorer

Theorem islmib

Description: Property of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019)

Ref Expression
Hypotheses ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismid.d ⊢ − = ( dist ‘ 𝐺 )
ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
lmif.m ⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
lmif.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
lmif.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
lmicl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
islmib.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
Assertion islmib ( 𝜑 → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ) )

Proof

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 eqtrid ⊢ ( 𝜑 → 𝑀 = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( 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 ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ) )