Metamath Proof Explorer

Theorem islmib

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

Ref Expression
Hypotheses ismid.p ⊢ P = Base G
ismid.d ⊢ - ˙ = dist ⁡ G
ismid.i ⊢ I = Itv ⁡ G
ismid.g ⊢ φ → G ∈ 𝒢 Tarski
ismid.1 ⊢ φ → G Dim 𝒢 ≥ 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 ↔ A mid 𝒢 ⁡ G B ∈ D ∧ D ⟂ 𝒢 ⁡ G A L B ∨ A = B

Proof

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