Metamath Proof Explorer

Theorem iseqlg

Description: Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020)

Ref Expression
Hypotheses iseqlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
iseqlg.m ⊢ − = ( dist ‘ 𝐺 )
iseqlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
iseqlg.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
iseqlg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
iseqlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
iseqlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
iseqlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
Assertion iseqlg ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( eqltrG ‘ 𝐺 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐴 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 iseqlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 iseqlg.m ⊢ − = ( dist ‘ 𝐺 )
3 iseqlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 iseqlg.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 iseqlg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 iseqlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 iseqlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 iseqlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 elex ⊢ ( 𝐺 ∈ TarskiG → 𝐺 ∈ V )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
11 10 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
12 11 oveq1d ⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
13 fveq2 ⊢ ( 𝑔 = 𝐺 → ( cgrG ‘ 𝑔 ) = ( cgrG ‘ 𝐺 ) )
14 13 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ ↔ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ ) )
15 12 14 rabeqbidv ⊢ ( 𝑔 = 𝐺 → { 𝑥 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } = { 𝑥 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } )
16 df-eqlg ⊢ eqltrG = ( 𝑔 ∈ V ↦ { 𝑥 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } )
17 ovex ⊢ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V
18 17 rabex ⊢ { 𝑥 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } ∈ V
19 15 16 18 fvmpt ⊢ ( 𝐺 ∈ V → ( eqltrG ‘ 𝐺 ) = { 𝑥 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } )
20 5 9 19 3syl ⊢ ( 𝜑 → ( eqltrG ‘ 𝐺 ) = { 𝑥 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } )
21 20 eleq2d ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( eqltrG ‘ 𝐺 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ { 𝑥 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } ) )
22 id ⊢ ( 𝑥 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → 𝑥 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
23 fveq1 ⊢ ( 𝑥 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑥 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
24 fveq1 ⊢ ( 𝑥 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑥 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
25 fveq1 ⊢ ( 𝑥 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑥 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
26 23 24 25 s3eqd ⊢ ( 𝑥 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ = ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ )
27 22 26 breq12d ⊢ ( 𝑥 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ ) )
28 27 elrab ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ { 𝑥 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ ) )
29 28 a1i ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ { 𝑥 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝐺 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ ) ) )
30 6 7 8 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
31 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
32 1 fvexi ⊢ 𝑃 ∈ V
33 3nn0 ⊢ 3 ∈ ℕ0
34 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
35 32 33 34 mp2an ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
36 30 31 35 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
37 36 biantrurd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ ) ) )
38 s3fv1 ⊢ ( 𝐵 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
39 7 38 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
40 s3fv2 ⊢ ( 𝐶 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
41 8 40 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
42 s3fv0 ⊢ ( 𝐴 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
43 6 42 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
44 39 41 43 s3eqd ⊢ ( 𝜑 → ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ = ⟨“ 𝐵 𝐶 𝐴 ”⟩ )
45 44 breq2d ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐴 ”⟩ ) )
46 37 45 bitr3d ⊢ ( 𝜑 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ”⟩ ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐴 ”⟩ ) )
47 21 29 46 3bitrd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( eqltrG ‘ 𝐺 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐴 ”⟩ ) )