Metamath Proof Explorer

Theorem israg

Description: Property for 3 points A, B, C to form a right angle. Definition 8.1 of Schwabhauser p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019)

Ref Expression
Hypotheses israg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
israg.d ⊢ − = ( dist ‘ 𝐺 )
israg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
israg.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
israg.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
israg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
israg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
israg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
israg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
Assertion israg ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 israg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 israg.d ⊢ − = ( dist ‘ 𝐺 )
3 israg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 israg.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 israg.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6 israg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 israg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 israg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 israg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10 7 8 9 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
11 fveqeq2 ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( ( ♯ ‘ 𝑤 ) = 3 ↔ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) )
12 fveq1 ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑤 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
13 fveq1 ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑤 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
14 12 13 oveq12d ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) )
15 fveq1 ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑤 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
16 15 fveq2d ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) = ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
17 16 13 fveq12d ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) = ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) )
18 12 17 oveq12d ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) )
19 14 18 eqeq12d ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) )
20 11 19 anbi12d ⊢ ( 𝑤 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) ↔ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) ) )
21 20 elrab3 ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ { 𝑤 ∈ Word 𝑃 ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } ↔ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) ) )
22 10 21 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ { 𝑤 ∈ Word 𝑃 ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } ↔ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) ) )
23 df-rag ⊢ ∟G = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Base ‘ 𝑔 ) ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
25 24 fveq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
26 25 1 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( Base ‘ 𝑔 ) = 𝑃 )
27 wrdeq ⊢ ( ( Base ‘ 𝑔 ) = 𝑃 → Word ( Base ‘ 𝑔 ) = Word 𝑃 )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → Word ( Base ‘ 𝑔 ) = Word 𝑃 )
29 24 fveq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) )
30 29 2 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( dist ‘ 𝑔 ) = − )
31 30 oveqd ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) )
32 eqidd ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( 𝑤 ‘ 0 ) = ( 𝑤 ‘ 0 ) )
33 24 fveq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( pInvG ‘ 𝑔 ) = ( pInvG ‘ 𝐺 ) )
34 33 5 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( pInvG ‘ 𝑔 ) = 𝑆 )
35 34 fveq1d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) = ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) )
36 35 fveq1d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) = ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) )
37 30 32 36 oveq123d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) )
38 31 37 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ↔ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) )
39 38 anbi2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) ↔ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) ) )
40 28 39 rabeqbidv ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → { 𝑤 ∈ Word ( Base ‘ 𝑔 ) ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } = { 𝑤 ∈ Word 𝑃 ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } )
41 6 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
42 1 fvexi ⊢ 𝑃 ∈ V
43 42 wrdexi ⊢ Word 𝑃 ∈ V
44 43 rabex ⊢ { 𝑤 ∈ Word 𝑃 ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } ∈ V
45 44 a1i ⊢ ( 𝜑 → { 𝑤 ∈ Word 𝑃 ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } ∈ V )
46 23 40 41 45 fvmptd2 ⊢ ( 𝜑 → ( ∟G ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑃 ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } )
47 46 eleq2d ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ { 𝑤 ∈ Word 𝑃 ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) − ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) − ( ( 𝑆 ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } ) )
48 s3fv0 ⊢ ( 𝐴 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
49 7 48 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
50 49 eqcomd ⊢ ( 𝜑 → 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
51 s3fv2 ⊢ ( 𝐶 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
52 9 51 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
53 52 eqcomd ⊢ ( 𝜑 → 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
54 50 53 oveq12d ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) )
55 s3fv1 ⊢ ( 𝐵 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
56 8 55 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
57 56 eqcomd ⊢ ( 𝜑 → 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
58 57 fveq2d ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
59 58 53 fveq12d ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) = ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) )
60 50 59 oveq12d ⊢ ( 𝜑 → ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) )
61 54 60 eqeq12d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) )
62 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
63 62 a1i ⊢ ( 𝜑 → ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 )
64 63 biantrurd ⊢ ( 𝜑 → ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ↔ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) ) )
65 61 64 bitrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ↔ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) − ( ( 𝑆 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) ) )
66 22 47 65 3bitr4d ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) )