Metamath Proof Explorer

Theorem islmib

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

Ref Expression
Hypotheses ismid.p ⊢P=BaseG
ismid.d ⊢-˙=dist⁡G
ismid.i ⊢I=Itv⁡G
ismid.g ⊢φ→G∈𝒢Tarski
ismid.1 ⊢φ→GDim𝒢≥2
lmif.m ⊢M=lInv𝒢⁡G⁡D
lmif.l ⊢L=Line𝒢⁡G
lmif.d ⊢φ→D∈ran⁡L
lmicl.1 ⊢φ→A∈P
islmib.b ⊢φ→B∈P
Assertion islmib ⊢φ→B=M⁡A↔Amid𝒢⁡GB∈D∧D⟂𝒢⁡GALB∨A=B

Proof

Step Hyp Ref Expression
1 ismid.p ⊢P=BaseG
2 ismid.d ⊢-˙=dist⁡G
3 ismid.i ⊢I=Itv⁡G
4 ismid.g ⊢φ→G∈𝒢Tarski
5 ismid.1 ⊢φ→GDim𝒢≥2
6 lmif.m ⊢M=lInv𝒢⁡G⁡D
7 lmif.l ⊢L=Line𝒢⁡G
8 lmif.d ⊢φ→D∈ran⁡L
9 lmicl.1 ⊢φ→A∈P
10 islmib.b ⊢φ→B∈P
11 df-lmi ⊢lInv𝒢=g∈V⟼d∈ran⁡Line𝒢⁡g⟼a∈Baseg⟼ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b
12 fveq2 ⊢g=G→Line𝒢⁡g=Line𝒢⁡G
13 12 7 eqtr4di ⊢g=G→Line𝒢⁡g=L
14 13 rneqd ⊢g=G→ran⁡Line𝒢⁡g=ran⁡L
15 fveq2 ⊢g=G→Baseg=BaseG
16 15 1 eqtr4di ⊢g=G→Baseg=P
17 fveq2 ⊢g=G→mid𝒢⁡g=mid𝒢⁡G
18 17 oveqd ⊢g=G→amid𝒢⁡gb=amid𝒢⁡Gb
19 18 eleq1d ⊢g=G→amid𝒢⁡gb∈d↔amid𝒢⁡Gb∈d
20 eqidd ⊢g=G→d=d
21 fveq2 ⊢g=G→⟂𝒢⁡g=⟂𝒢⁡G
22 13 oveqd ⊢g=G→aLine𝒢⁡gb=aLb
23 20 21 22 breq123d ⊢g=G→d⟂𝒢⁡gaLine𝒢⁡gb↔d⟂𝒢⁡GaLb
24 23 orbi1d ⊢g=G→d⟂𝒢⁡gaLine𝒢⁡gb∨a=b↔d⟂𝒢⁡GaLb∨a=b
25 19 24 anbi12d ⊢g=G→amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b↔amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
26 16 25 riotaeqbidv ⊢g=G→ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b=ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
27 16 26 mpteq12dv ⊢g=G→a∈Baseg⟼ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b=a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
28 14 27 mpteq12dv ⊢g=G→d∈ran⁡Line𝒢⁡g⟼a∈Baseg⟼ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b=d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
29 4 elexd ⊢φ→G∈V
30 7 fvexi ⊢L∈V
31 rnexg ⊢L∈V→ran⁡L∈V
32 mptexg ⊢ran⁡L∈V→d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b∈V
33 30 31 32 mp2b ⊢d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b∈V
34 33 a1i ⊢φ→d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b∈V
35 11 28 29 34 fvmptd3 ⊢φ→lInv𝒢⁡G=d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
36 eleq2 ⊢d=D→amid𝒢⁡Gb∈d↔amid𝒢⁡Gb∈D
37 breq1 ⊢d=D→d⟂𝒢⁡GaLb↔D⟂𝒢⁡GaLb
38 37 orbi1d ⊢d=D→d⟂𝒢⁡GaLb∨a=b↔D⟂𝒢⁡GaLb∨a=b
39 36 38 anbi12d ⊢d=D→amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b↔amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
40 39 riotabidv ⊢d=D→ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b=ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
41 40 mpteq2dv ⊢d=D→a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
42 41 adantl ⊢φ∧d=D→a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
43 1 fvexi ⊢P∈V
44 43 mptex ⊢a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b∈V
45 44 a1i ⊢φ→a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b∈V
46 35 42 8 45 fvmptd ⊢φ→lInv𝒢⁡G⁡D=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
47 6 46 eqtrid ⊢φ→M=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
48 oveq1 ⊢a=A→amid𝒢⁡Gb=Amid𝒢⁡Gb
49 48 eleq1d ⊢a=A→amid𝒢⁡Gb∈D↔Amid𝒢⁡Gb∈D
50 oveq1 ⊢a=A→aLb=ALb
51 50 breq2d ⊢a=A→D⟂𝒢⁡GaLb↔D⟂𝒢⁡GALb
52 eqeq1 ⊢a=A→a=b↔A=b
53 51 52 orbi12d ⊢a=A→D⟂𝒢⁡GaLb∨a=b↔D⟂𝒢⁡GALb∨A=b
54 49 53 anbi12d ⊢a=A→amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b↔Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b
55 54 riotabidv ⊢a=A→ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b=ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b
56 55 adantl ⊢φ∧a=A→ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b=ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b
57 1 2 3 4 5 7 8 9 lmieu ⊢φ→∃!b∈PAmid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b
58 riotacl ⊢∃!b∈PAmid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b→ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b∈P
59 57 58 syl ⊢φ→ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b∈P
60 47 56 9 59 fvmptd ⊢φ→M⁡A=ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b
61 60 eqeq2d ⊢φ→B=M⁡A↔B=ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b
62 oveq2 ⊢b=B→Amid𝒢⁡Gb=Amid𝒢⁡GB
63 62 eleq1d ⊢b=B→Amid𝒢⁡Gb∈D↔Amid𝒢⁡GB∈D
64 oveq2 ⊢b=B→ALb=ALB
65 64 breq2d ⊢b=B→D⟂𝒢⁡GALb↔D⟂𝒢⁡GALB
66 eqeq2 ⊢b=B→A=b↔A=B
67 65 66 orbi12d ⊢b=B→D⟂𝒢⁡GALb∨A=b↔D⟂𝒢⁡GALB∨A=B
68 63 67 anbi12d ⊢b=B→Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b↔Amid𝒢⁡GB∈D∧D⟂𝒢⁡GALB∨A=B
69 68 riota2 ⊢B∈P∧∃!b∈PAmid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b→Amid𝒢⁡GB∈D∧D⟂𝒢⁡GALB∨A=B↔ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b=B
70 10 57 69 syl2anc ⊢φ→Amid𝒢⁡GB∈D∧D⟂𝒢⁡GALB∨A=B↔ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b=B
71 eqcom ⊢B=ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b↔ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b=B
72 70 71 bitr4di ⊢φ→Amid𝒢⁡GB∈D∧D⟂𝒢⁡GALB∨A=B↔B=ιb∈P|Amid𝒢⁡Gb∈D∧D⟂𝒢⁡GALb∨A=b
73 61 72 bitr4d ⊢φ→B=M⁡A↔Amid𝒢⁡GB∈D∧D⟂𝒢⁡GALB∨A=B