Metamath Proof Explorer

Theorem mirbtwnhl

Description: If the center of the point inversion A is between two points X and Y , then the half lines are mirrored. (Contributed by Thierry Arnoux, 3-Mar-2020)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirhl.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
mirhl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
mirhl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
mirhl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
mirhl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
mirhl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
mirbtwnhl.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝐴 )
mirbtwnhl.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝐴 )
mirbtwnhl.3 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 𝑌 ) )
Assertion mirbtwnhl ( 𝜑 → ( 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ↔ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d ⊢ − = ( dist ‘ 𝐺 )
3 mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 mirhl.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
8 mirhl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
9 mirhl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 mirhl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11 mirhl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
12 mirhl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
13 mirbtwnhl.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝐴 )
14 mirbtwnhl.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝐴 )
15 mirbtwnhl.3 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 𝑌 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → 𝑍 = 𝐴 )
17 1 3 8 9 10 9 6 hleqnid ⊢ ( 𝜑 → ¬ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝑋 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ¬ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝑋 )
19 16 18 eqnbrtrd ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ¬ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 )
20 16 fveq2d ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ( 𝑀 ‘ 𝑍 ) = ( 𝑀 ‘ 𝐴 ) )
21 1 2 3 4 5 6 9 7 mircinv ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
23 20 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ( 𝑀 ‘ 𝑍 ) = 𝐴 )
24 1 3 8 9 11 9 6 hleqnid ⊢ ( 𝜑 → ¬ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝑌 )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ¬ 𝐴 ( 𝐾 ‘ 𝐴 ) 𝑌 )
26 23 25 eqnbrtrd ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ¬ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 )
27 19 26 2falsed ⊢ ( ( 𝜑 ∧ 𝑍 = 𝐴 ) → ( 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ↔ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝑍 ≠ 𝐴 )
29 28 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ¬ 𝑍 = 𝐴 )
30 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) ∧ ( 𝑀 ‘ 𝑍 ) = 𝐴 ) → 𝐺 ∈ TarskiG )
31 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) ∧ ( 𝑀 ‘ 𝑍 ) = 𝐴 ) → 𝐴 ∈ 𝑃 )
32 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) ∧ ( 𝑀 ‘ 𝑍 ) = 𝐴 ) → 𝑍 ∈ 𝑃 )
33 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) ∧ ( 𝑀 ‘ 𝑍 ) = 𝐴 ) → ( 𝑀 ‘ 𝑍 ) = 𝐴 )
34 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) ∧ ( 𝑀 ‘ 𝑍 ) = 𝐴 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
35 33 34 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) ∧ ( 𝑀 ‘ 𝑍 ) = 𝐴 ) → ( 𝑀 ‘ 𝑍 ) = ( 𝑀 ‘ 𝐴 ) )
36 1 2 3 4 5 30 31 7 32 31 35 mireq ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) ∧ ( 𝑀 ‘ 𝑍 ) = 𝐴 ) → 𝑍 = 𝐴 )
37 29 36 mtand ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ¬ ( 𝑀 ‘ 𝑍 ) = 𝐴 )
38 37 neqned ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( 𝑀 ‘ 𝑍 ) ≠ 𝐴 )
39 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝑌 ≠ 𝐴 )
40 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝐺 ∈ TarskiG )
41 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝑋 ∈ 𝑃 )
42 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝐴 ∈ 𝑃 )
43 1 2 3 4 5 6 9 7 12 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) ∈ 𝑃 )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( 𝑀 ‘ 𝑍 ) ∈ 𝑃 )
45 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝑌 ∈ 𝑃 )
46 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝑋 ≠ 𝐴 )
47 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝑍 ∈ 𝑃 )
48 1 3 8 12 10 9 6 ishlg ⊢ ( 𝜑 → ( 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ↔ ( 𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ ( 𝑍 ∈ ( 𝐴 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐴 𝐼 𝑍 ) ) ) ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) → ( 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ↔ ( 𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ ( 𝑍 ∈ ( 𝐴 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐴 𝐼 𝑍 ) ) ) ) )
50 49 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( 𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ ( 𝑍 ∈ ( 𝐴 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐴 𝐼 𝑍 ) ) ) )
51 50 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( 𝑍 ∈ ( 𝐴 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐴 𝐼 𝑍 ) ) )
52 51 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( 𝑋 ∈ ( 𝐴 𝐼 𝑍 ) ∨ 𝑍 ∈ ( 𝐴 𝐼 𝑋 ) ) )
53 1 2 3 4 5 40 7 42 41 47 52 mirconn ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀 ‘ 𝑍 ) ) )
54 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → 𝐴 ∈ ( 𝑋 𝐼 𝑌 ) )
55 1 3 40 41 42 44 45 46 53 54 tgbtwnconn2 ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( ( 𝑀 ‘ 𝑍 ) ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) )
56 1 3 8 43 11 9 6 ishlg ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ↔ ( ( 𝑀 ‘ 𝑍 ) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ( ( 𝑀 ‘ 𝑍 ) ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) → ( ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ↔ ( ( 𝑀 ‘ 𝑍 ) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ( ( 𝑀 ‘ 𝑍 ) ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) ) ) )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ↔ ( ( 𝑀 ‘ 𝑍 ) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ( ( 𝑀 ‘ 𝑍 ) ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) ) ) )
59 38 39 55 58 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ) → ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 )
60 simplr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝑍 ≠ 𝐴 )
61 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝑋 ≠ 𝐴 )
62 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝐺 ∈ TarskiG )
63 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝑌 ∈ 𝑃 )
64 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝐴 ∈ 𝑃 )
65 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝑍 ∈ 𝑃 )
66 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝑋 ∈ 𝑃 )
67 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝑌 ≠ 𝐴 )
68 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
69 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( 𝑀 ‘ 𝑍 ) ∈ 𝑃 )
70 1 2 3 4 5 62 64 7 63 mircl ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
71 57 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( ( 𝑀 ‘ 𝑍 ) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ( ( 𝑀 ‘ 𝑍 ) ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) ) )
72 71 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( ( 𝑀 ‘ 𝑍 ) ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) )
73 1 2 3 4 5 62 7 64 69 63 72 mirconn ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝐴 ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑌 ) ) )
74 1 2 3 62 69 64 70 73 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝐴 ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) )
75 68 74 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) )
76 1 2 3 4 5 62 64 7 63 64 65 mirbtwnb ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( 𝐴 ∈ ( 𝑌 𝐼 𝑍 ) ↔ ( 𝑀 ‘ 𝐴 ) ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) )
77 75 76 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝐴 ∈ ( 𝑌 𝐼 𝑍 ) )
78 1 2 3 6 10 9 11 15 tgbtwncom ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑌 𝐼 𝑋 ) )
79 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝐴 ∈ ( 𝑌 𝐼 𝑋 ) )
80 1 3 62 63 64 65 66 67 77 79 tgbtwnconn2 ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( 𝑍 ∈ ( 𝐴 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐴 𝐼 𝑍 ) ) )
81 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → ( 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ↔ ( 𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ ( 𝑍 ∈ ( 𝐴 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐴 𝐼 𝑍 ) ) ) ) )
82 60 61 80 81 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) ∧ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) → 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 )
83 59 82 impbida ⊢ ( ( 𝜑 ∧ 𝑍 ≠ 𝐴 ) → ( 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ↔ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) )
84 27 83 pm2.61dane ⊢ ( 𝜑 → ( 𝑍 ( 𝐾 ‘ 𝐴 ) 𝑋 ↔ ( 𝑀 ‘ 𝑍 ) ( 𝐾 ‘ 𝐴 ) 𝑌 ) )