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 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 ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ) )