Metamath Proof Explorer

Theorem hypcgrlem2

Description: Lemma for hypcgr , case where triangles share one vertex B . (Contributed by Thierry Arnoux, 16-Dec-2019)

Ref Expression
Hypotheses hypcgr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
hypcgr.m ⊢ − = ( dist ‘ 𝐺 )
hypcgr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
hypcgr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hypcgr.h ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
hypcgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
hypcgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
hypcgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
hypcgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
hypcgr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
hypcgr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
hypcgr.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
hypcgr.2 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
hypcgr.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
hypcgr.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
hypcgrlem2.b ⊢ ( 𝜑 → 𝐵 = 𝐸 )
hypcgrlem2.s ⊢ 𝑆 = ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) )
Assertion hypcgrlem2 ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )

Proof

Step Hyp Ref Expression
1 hypcgr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 hypcgr.m ⊢ − = ( dist ‘ 𝐺 )
3 hypcgr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 hypcgr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 hypcgr.h ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
6 hypcgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 hypcgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 hypcgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 hypcgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 hypcgr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 hypcgr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 hypcgr.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
13 hypcgr.2 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
14 hypcgr.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
15 hypcgr.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
16 hypcgrlem2.b ⊢ ( 𝜑 → 𝐵 = 𝐸 )
17 hypcgrlem2.s ⊢ 𝑆 = ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) )
18 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐺 ∈ TarskiG )
19 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐺 DimTarskiG≥ 2 )
20 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐴 ∈ 𝑃 )
21 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐵 ∈ 𝑃 )
22 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐶 ∈ 𝑃 )
23 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
24 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
25 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 )
26 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐷 ∈ 𝑃 )
27 1 2 3 23 24 18 21 25 26 mircl ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) ∈ 𝑃 )
28 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐸 ∈ 𝑃 )
29 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
30 eqidd ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) )
31 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐵 = 𝐸 )
32 1 2 3 23 24 18 21 25 28 mirinv ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐸 ) = 𝐸 ↔ 𝐵 = 𝐸 ) )
33 31 32 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐸 ) = 𝐸 )
34 33 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐸 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐸 ) )
35 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐹 ∈ 𝑃 )
36 1 2 3 18 19 22 35 midcom ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = ( 𝐹 ( midG ‘ 𝐺 ) 𝐶 ) )
37 simpr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 )
38 36 37 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐹 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐵 )
39 1 2 3 18 19 35 22 24 21 ismidb ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐹 ) ↔ ( 𝐹 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐵 ) )
40 38 39 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐹 ) )
41 30 34 40 s3eqd ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) 𝐸 𝐶 ”⟩ = ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐸 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐹 ) ”⟩ )
42 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
43 1 2 3 23 24 18 26 28 35 42 25 21 mirrag ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐸 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐹 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
44 41 43 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) 𝐸 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
45 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
46 1 2 3 23 24 18 21 25 26 28 miriso ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐸 ) ) = ( 𝐷 − 𝐸 ) )
47 33 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐸 ) ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − 𝐸 ) )
48 45 46 47 3eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐴 − 𝐵 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − 𝐸 ) )
49 31 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐶 ) )
50 eqid ⊢ ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) ) ( LineG ‘ 𝐺 ) 𝐵 ) ) = ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) ) ( LineG ‘ 𝐺 ) 𝐵 ) )
51 eqidd ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → 𝐶 = 𝐶 )
52 1 2 3 18 19 20 21 22 27 28 22 29 44 48 49 31 50 51 hypcgrlem1 ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐴 − 𝐶 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − 𝐶 ) )
53 40 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − 𝐶 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐹 ) ) )
54 1 2 3 23 24 18 21 25 26 35 miriso ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐹 ) ) = ( 𝐷 − 𝐹 ) )
55 52 53 54 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐵 ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
56 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐺 ∈ TarskiG )
57 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐺 DimTarskiG≥ 2 )
58 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐴 ∈ 𝑃 )
59 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐵 ∈ 𝑃 )
60 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐶 ∈ 𝑃 )
61 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐷 ∈ 𝑃 )
62 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐸 ∈ 𝑃 )
63 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐹 ∈ 𝑃 )
64 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
65 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
66 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
67 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
68 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐵 = 𝐸 )
69 eqid ⊢ ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐷 ) ( LineG ‘ 𝐺 ) 𝐵 ) ) = ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐷 ) ( LineG ‘ 𝐺 ) 𝐵 ) )
70 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → 𝐶 = 𝐹 )
71 1 2 3 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 hypcgrlem1 ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = 𝐹 ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
72 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐺 ∈ TarskiG )
73 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐺 DimTarskiG≥ 2 )
74 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐴 ∈ 𝑃 )
75 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐵 ∈ 𝑃 )
76 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐶 ∈ 𝑃 )
77 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐹 ∈ 𝑃 )
78 1 2 3 72 73 76 77 midcl ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ∈ 𝑃 )
79 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 )
80 1 3 23 72 78 75 79 tgelrnln ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) ∈ ran ( LineG ‘ 𝐺 ) )
81 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐷 ∈ 𝑃 )
82 1 2 3 72 73 17 23 80 81 lmicl ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝑆 ‘ 𝐷 ) ∈ 𝑃 )
83 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐸 ∈ 𝑃 )
84 1 2 3 72 73 17 23 80 83 lmicl ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝑆 ‘ 𝐸 ) ∈ 𝑃 )
85 1 2 3 72 73 17 23 80 77 lmicl ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝑆 ‘ 𝐹 ) ∈ 𝑃 )
86 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
87 1 2 3 72 73 17 23 80 lmimot ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝑆 ∈ ( 𝐺 Ismt 𝐺 ) )
88 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
89 1 2 3 23 24 72 81 83 77 87 88 motrag ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ⟨“ ( 𝑆 ‘ 𝐷 ) ( 𝑆 ‘ 𝐸 ) ( 𝑆 ‘ 𝐹 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
90 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
91 1 2 3 72 73 17 23 80 81 83 lmiiso ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( ( 𝑆 ‘ 𝐷 ) − ( 𝑆 ‘ 𝐸 ) ) = ( 𝐷 − 𝐸 ) )
92 90 91 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐴 − 𝐵 ) = ( ( 𝑆 ‘ 𝐷 ) − ( 𝑆 ‘ 𝐸 ) ) )
93 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
94 1 2 3 72 73 17 23 80 83 77 lmiiso ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( ( 𝑆 ‘ 𝐸 ) − ( 𝑆 ‘ 𝐹 ) ) = ( 𝐸 − 𝐹 ) )
95 93 94 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐵 − 𝐶 ) = ( ( 𝑆 ‘ 𝐸 ) − ( 𝑆 ‘ 𝐹 ) ) )
96 1 3 23 72 78 75 79 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐵 ∈ ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) )
97 1 2 3 72 73 17 23 80 75 96 lmicinv ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝑆 ‘ 𝐵 ) = 𝐵 )
98 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐵 = 𝐸 )
99 98 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐸 ) )
100 97 99 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐵 = ( 𝑆 ‘ 𝐸 ) )
101 eqid ⊢ ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐷 ) ) ( LineG ‘ 𝐺 ) 𝐵 ) ) = ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐷 ) ) ( LineG ‘ 𝐺 ) 𝐵 ) )
102 1 2 3 72 73 76 77 midcom ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = ( 𝐹 ( midG ‘ 𝐺 ) 𝐶 ) )
103 1 3 23 72 78 75 79 tglinerflx1 ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ∈ ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) )
104 102 103 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐹 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) )
105 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐶 ≠ 𝐹 )
106 105 necomd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐹 ≠ 𝐶 )
107 1 3 23 72 77 76 106 tgelrnln ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐹 ( LineG ‘ 𝐺 ) 𝐶 ) ∈ ran ( LineG ‘ 𝐺 ) )
108 1 2 3 72 73 76 77 midbtwn ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ∈ ( 𝐶 𝐼 𝐹 ) )
109 1 2 3 72 76 78 77 108 tgbtwncom ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ∈ ( 𝐹 𝐼 𝐶 ) )
110 1 3 23 72 77 76 78 106 109 btwnlng1 ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ∈ ( 𝐹 ( LineG ‘ 𝐺 ) 𝐶 ) )
111 103 110 elind ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ∈ ( ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) ∩ ( 𝐹 ( LineG ‘ 𝐺 ) 𝐶 ) ) )
112 1 3 23 72 77 76 106 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐶 ∈ ( 𝐹 ( LineG ‘ 𝐺 ) 𝐶 ) )
113 79 necomd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐵 ≠ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) )
114 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
115 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → 𝐶 ∈ 𝑃 )
116 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → 𝐹 ∈ 𝑃 )
117 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → 𝐺 DimTarskiG≥ 2 )
118 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) )
119 118 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = 𝐶 )
120 1 2 3 114 117 115 116 119 midcgr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → ( 𝐶 − 𝐶 ) = ( 𝐶 − 𝐹 ) )
121 120 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐶 ) )
122 1 2 3 114 115 116 115 121 axtgcgrid ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) → 𝐶 = 𝐹 )
123 122 ex ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) → ( 𝐶 = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) → 𝐶 = 𝐹 ) )
124 123 necon3d ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) → ( 𝐶 ≠ 𝐹 → 𝐶 ≠ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) )
125 124 imp ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐶 ≠ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) )
126 98 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐸 = 𝐵 )
127 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) )
128 1 2 3 72 73 76 77 24 78 ismidb ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐹 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) ‘ 𝐶 ) ↔ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) = ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) )
129 127 128 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐹 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) ‘ 𝐶 ) )
130 126 129 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐸 − 𝐹 ) = ( 𝐵 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) ‘ 𝐶 ) ) )
131 93 130 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐵 − 𝐶 ) = ( 𝐵 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) ‘ 𝐶 ) ) )
132 1 2 3 23 24 72 75 78 76 israg ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( ⟨“ 𝐵 ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐵 − 𝐶 ) = ( 𝐵 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ) ‘ 𝐶 ) ) ) )
133 131 132 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ⟨“ 𝐵 ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
134 1 2 3 23 72 80 107 111 96 112 113 125 133 ragperp ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐹 ( LineG ‘ 𝐺 ) 𝐶 ) )
135 134 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐹 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐹 = 𝐶 ) )
136 1 2 3 72 73 17 23 80 77 76 islmib ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐶 = ( 𝑆 ‘ 𝐹 ) ↔ ( ( 𝐹 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) ∧ ( ( ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ( LineG ‘ 𝐺 ) 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐹 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐹 = 𝐶 ) ) ) )
137 104 135 136 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → 𝐶 = ( 𝑆 ‘ 𝐹 ) )
138 1 2 3 72 73 74 75 76 82 84 85 86 89 92 95 100 101 137 hypcgrlem1 ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐴 − 𝐶 ) = ( ( 𝑆 ‘ 𝐷 ) − ( 𝑆 ‘ 𝐹 ) ) )
139 1 2 3 72 73 17 23 80 81 77 lmiiso ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( ( 𝑆 ‘ 𝐷 ) − ( 𝑆 ‘ 𝐹 ) ) = ( 𝐷 − 𝐹 ) )
140 138 139 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐹 ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
141 71 140 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝐶 ( midG ‘ 𝐺 ) 𝐹 ) ≠ 𝐵 ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
142 55 141 pm2.61dane ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )