Metamath Proof Explorer

Theorem prlngmid2

Description: If the midpoints of two segments ( X I Z ) and ( Y I W ) coincide, the points X , Y , Z and W form a parallelogram, i.e. the lines ( X L Y ) and ( Z L W ) are parallel. Theorem 12.17 of Schwabhauser p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses prlngmid2.b ⊢ 𝑃 = ( Base ‘ 𝐺 )
prlngmid2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
prlngmid2.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
prlngmid2.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
prlngmid2.m ⊢ 𝑀 = ( midG ‘ 𝐺 )
prlngmid2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
prlngmid2.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
prlngmid2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
prlngmid2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
prlngmid2.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
prlngmid2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
prlngmid2.2 ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) = ( 𝑌 𝑀 𝑊 ) )
prlngmid2.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion prlngmid2 ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )

Proof

Step Hyp Ref Expression
1 prlngmid2.b ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 prlngmid2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 prlngmid2.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
4 prlngmid2.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
5 prlngmid2.m ⊢ 𝑀 = ( midG ‘ 𝐺 )
6 prlngmid2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 prlngmid2.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
8 prlngmid2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9 prlngmid2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10 prlngmid2.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
11 prlngmid2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
12 prlngmid2.2 ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) = ( 𝑌 𝑀 𝑊 ) )
13 prlngmid2.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
14 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
15 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
16 1 15 2 6 8 9 13 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
17 1 2 3 6 16 10 tgelrnpln ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) ∈ ran 𝐸 )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) ∈ ran 𝐸 )
19 1 15 2 3 6 16 10 elplnglnid ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
21 1 15 2 3 6 16 10 elplngid ⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
22 12 fveq2d ⊢ ( 𝜑 → ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑌 𝑀 𝑊 ) ) )
23 22 fveq1d ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑌 𝑀 𝑊 ) ) ‘ 𝑌 ) )
24 5 oveqi ⊢ ( 𝑌 𝑀 𝑊 ) = ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 )
25 24 eqcomi ⊢ ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = ( 𝑌 𝑀 𝑊 )
26 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
27 10 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
28 10 eldifbd ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
29 13 neneqd ⊢ ( 𝜑 → ¬ 𝑋 = 𝑌 )
30 ioran ⊢ ( ¬ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑋 = 𝑌 ) )
31 28 29 30 sylanbrc ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
32 1 2 15 6 8 9 27 31 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
33 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
34 5 oveqi ⊢ ( 𝑋 𝑀 𝑍 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 )
35 1 26 15 6 32 8 27 midcl ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ 𝑃 )
36 34 35 eqeltrid ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) ∈ 𝑃 )
37 12 36 eqeltrrd ⊢ ( 𝜑 → ( 𝑌 𝑀 𝑊 ) ∈ 𝑃 )
38 1 26 15 6 32 9 11 33 37 ismidb ⊢ ( 𝜑 → ( 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑌 𝑀 𝑊 ) ) ‘ 𝑌 ) ↔ ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = ( 𝑌 𝑀 𝑊 ) ) )
39 25 38 mpbiri ⊢ ( 𝜑 → 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑌 𝑀 𝑊 ) ) ‘ 𝑌 ) )
40 23 39 eqtr4d ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) = 𝑊 )
41 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) )
42 1 15 2 6 8 9 13 tglinerflx1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
43 19 42 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
44 nelne2 ⊢ ( ( 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑍 )
45 42 28 44 syl2anc ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
46 1 15 2 3 6 17 43 21 45 lnssplng1 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
47 1 26 15 6 32 8 27 midbtwn ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) )
48 34 47 eqeltrid ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) )
49 1 15 2 6 8 27 36 45 48 btwnlng1 ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑍 ) )
50 46 49 sseldd ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
51 1 15 2 6 8 9 13 tglinerflx2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
52 19 51 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
53 1 3 33 41 6 17 50 52 mirplncl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
54 40 53 eqeltrrd ⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
55 6 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → 𝐺 ∈ TarskiG )
56 36 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → ( 𝑋 𝑀 𝑍 ) ∈ 𝑃 )
57 8 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → 𝑋 ∈ 𝑃 )
58 9 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → 𝑌 ∈ 𝑃 )
59 34 eqcomi ⊢ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑋 𝑀 𝑍 )
60 1 26 15 6 32 8 27 33 36 ismidb ⊢ ( 𝜑 → ( 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) ↔ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑋 𝑀 𝑍 ) ) )
61 59 60 mpbiri ⊢ ( 𝜑 → 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) )
62 61 eqcomd ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) = 𝑍 )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) = 𝑍 )
64 simpr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → 𝑍 = 𝑊 )
65 40 eqcomd ⊢ ( 𝜑 → 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) )
67 63 64 66 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) )
68 1 26 15 2 33 55 56 41 57 58 67 mireq ⊢ ( ( 𝜑 ∧ 𝑍 = 𝑊 ) → 𝑋 = 𝑌 )
69 13 68 mteqand ⊢ ( 𝜑 → 𝑍 ≠ 𝑊 )
70 1 15 2 3 6 17 21 54 69 lnssplng1 ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
72 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
73 20 72 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
74 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
75 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑍 )
76 1 15 2 3 14 18 73 74 75 lnssplng1 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑍 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
77 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑍 ) )
78 76 77 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
79 simplr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) )
80 20 79 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑒 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
81 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
82 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ 𝑃 )
83 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ 𝑃 )
84 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ 𝑃 )
85 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → 𝑋 = ( 𝑋 𝑀 𝑍 ) )
86 85 34 eqtr2di ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = 𝑋 )
87 1 26 15 6 32 8 27 33 8 ismidb ⊢ ( 𝜑 → ( 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑋 ) ↔ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = 𝑋 ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → ( 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑋 ) ↔ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = 𝑋 ) )
89 86 88 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑋 ) )
90 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 )
91 1 26 15 2 33 6 8 90 mircinv ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑋 ) = 𝑋 )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑋 ) = 𝑋 )
93 89 92 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → 𝑋 = 𝑍 )
94 42 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
95 93 94 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑋 = ( 𝑋 𝑀 𝑍 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
96 28 95 mtand ⊢ ( 𝜑 → ¬ 𝑋 = ( 𝑋 𝑀 𝑍 ) )
97 96 neqned ⊢ ( 𝜑 → 𝑋 ≠ ( 𝑋 𝑀 𝑍 ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ ( 𝑋 𝑀 𝑍 ) )
99 1 15 2 6 8 27 45 tglinecom ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑋 ) )
100 49 99 eleqtrd ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑍 𝐿 𝑋 ) )
101 100 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑍 𝐿 𝑋 ) )
102 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑍 )
103 102 necomd ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ≠ 𝑋 )
104 1 15 2 81 82 83 84 98 101 103 lnrot1 ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ ( 𝑋 𝐿 ( 𝑋 𝑀 𝑍 ) ) )
105 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
106 42 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
107 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) )
108 1 15 2 81 82 83 98 98 105 106 107 tglinethru ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 𝐿 ( 𝑋 𝑀 𝑍 ) ) )
109 104 108 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
110 28 109 mtand ⊢ ( 𝜑 → ¬ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) )
111 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ¬ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) )
112 nelne2 ⊢ ( ( 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ ( 𝑋 𝑀 𝑍 ) ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑒 ≠ ( 𝑋 𝑀 𝑍 ) )
113 79 111 112 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑒 ≠ ( 𝑋 𝑀 𝑍 ) )
114 113 necomd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ≠ 𝑒 )
115 1 15 2 3 14 18 78 80 114 lnssplng1 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
116 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
117 1 2 15 14 116 79 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑒 ∈ 𝑃 )
118 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ 𝑃 )
119 1 15 2 14 117 118 113 tglinecom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑒 𝐿 ( 𝑋 𝑀 𝑍 ) ) = ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
120 1 15 2 14 117 118 113 tgelrnln ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑒 𝐿 ( 𝑋 𝑀 𝑍 ) ) ∈ ran 𝐿 )
121 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) )
122 119 121 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑒 𝐿 ( 𝑋 𝑀 𝑍 ) ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) )
123 1 26 15 2 14 120 116 122 perpcom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) ( 𝑒 𝐿 ( 𝑋 𝑀 𝑍 ) ) )
124 119 123 breq2dd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
125 14 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝐺 ∈ TarskiG )
126 1 15 2 6 27 11 69 tgelrnln ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
127 126 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
128 127 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
129 119 120 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ∈ ran 𝐿 )
130 129 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ∈ ran 𝐿 )
131 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) )
132 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ 𝑃 )
133 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
134 13 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
135 134 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ≠ 𝑋 )
136 1 2 33 41 14 118 117 132 133 135 79 mirlni ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) ) )
137 62 40 oveq12d ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) ) = ( 𝑍 𝐿 𝑊 ) )
138 137 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) ) = ( 𝑍 𝐿 𝑊 ) )
139 136 138 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ∈ ( 𝑍 𝐿 𝑊 ) )
140 1 15 2 14 118 117 114 tglinerflx1 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
141 1 15 2 14 118 117 114 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑒 ∈ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
142 1 26 15 2 33 14 41 129 140 141 mirln ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ∈ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
143 139 142 elind ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ∈ ( ( 𝑍 𝐿 𝑊 ) ∩ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ) )
144 143 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ∈ ( ( 𝑍 𝐿 𝑊 ) ∩ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ) )
145 131 144 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑍 ∈ ( ( 𝑍 𝐿 𝑊 ) ∩ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ) )
146 1 15 2 6 27 11 69 tglinerflx2 ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑍 𝐿 𝑊 ) )
147 146 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑊 ∈ ( 𝑍 𝐿 𝑊 ) )
148 140 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
149 69 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑍 )
150 149 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑊 ≠ 𝑍 )
151 1 26 15 2 33 14 118 41 117 113 mirne ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ≠ ( 𝑋 𝑀 𝑍 ) )
152 151 necomd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝑀 𝑍 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) )
153 152 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝑀 𝑍 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) )
154 153 131 neeqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝑀 𝑍 ) ≠ 𝑍 )
155 40 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) = 𝑊 )
156 131 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) = 𝑍 )
157 1 26 15 2 33 6 36 41 mircinv ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ ( 𝑋 𝑀 𝑍 ) ) = ( 𝑋 𝑀 𝑍 ) )
158 157 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ ( 𝑋 𝑀 𝑍 ) ) = ( 𝑋 𝑀 𝑍 ) )
159 158 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ ( 𝑋 𝑀 𝑍 ) ) = ( 𝑋 𝑀 𝑍 ) )
160 155 156 159 s3eqd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ ( 𝑋 𝑀 𝑍 ) ) ”⟩ = ⟨“ 𝑊 𝑍 ( 𝑋 𝑀 𝑍 ) ”⟩ )
161 133 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑌 ∈ 𝑃 )
162 117 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑒 ∈ 𝑃 )
163 118 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ 𝑃 )
164 132 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑋 ∈ 𝑃 )
165 1 15 2 14 133 132 117 135 79 lncom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑒 ∈ ( 𝑌 𝐿 𝑋 ) )
166 165 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑒 ∈ ( 𝑌 𝐿 𝑋 ) )
167 1 15 2 6 8 9 13 tglinecom ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑋 ) )
168 167 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑋 ) )
169 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
170 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) )
171 1 26 15 2 125 130 169 170 perpcom ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
172 168 171 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑌 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
173 119 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑒 𝐿 ( 𝑋 𝑀 𝑍 ) ) = ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
174 172 173 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑌 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) ( 𝑒 𝐿 ( 𝑋 𝑀 𝑍 ) ) )
175 1 26 15 2 125 161 164 166 163 174 perprag ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ⟨“ 𝑌 𝑒 ( 𝑋 𝑀 𝑍 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
176 1 26 15 2 33 125 161 162 163 175 41 163 mirrag ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑌 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ ( 𝑋 𝑀 𝑍 ) ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
177 160 176 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ⟨“ 𝑊 𝑍 ( 𝑋 𝑀 𝑍 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
178 1 26 15 2 125 128 130 145 147 148 150 154 177 ragperp ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑍 𝐿 𝑊 ) ( ⟂G ‘ 𝐺 ) ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
179 14 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝐺 ∈ TarskiG )
180 127 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
181 129 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ∈ ran 𝐿 )
182 143 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ∈ ( ( 𝑍 𝐿 𝑊 ) ∩ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ) )
183 1 15 2 6 27 11 69 tglinerflx1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
184 183 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
185 184 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
186 140 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝑀 𝑍 ) ∈ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
187 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) )
188 152 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑋 𝑀 𝑍 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) )
189 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) = 𝑍 )
190 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) )
191 189 190 158 s3eqd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ ( 𝑋 𝑀 𝑍 ) ) ”⟩ = ⟨“ 𝑍 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ( 𝑋 𝑀 𝑍 ) ”⟩ )
192 1 26 15 2 14 132 133 79 118 123 perprag ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ⟨“ 𝑋 𝑒 ( 𝑋 𝑀 𝑍 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
193 1 26 15 2 33 14 132 117 118 192 41 118 mirrag ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑋 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ ( 𝑋 𝑀 𝑍 ) ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
194 191 193 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ⟨“ 𝑍 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ( 𝑋 𝑀 𝑍 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
195 194 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ⟨“ 𝑍 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ( 𝑋 𝑀 𝑍 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
196 1 26 15 2 179 180 181 182 185 186 187 188 195 ragperp ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑍 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 𝑀 𝑍 ) ) ‘ 𝑒 ) ) → ( 𝑍 𝐿 𝑊 ) ( ⟂G ‘ 𝐺 ) ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
197 178 196 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑊 ) ( ⟂G ‘ 𝐺 ) ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) )
198 1 2 3 4 14 18 20 71 115 124 197 perpprlng ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
199 1 26 15 2 6 16 36 110 footex ⊢ ( 𝜑 → ∃ 𝑒 ∈ ( 𝑋 𝐿 𝑌 ) ( ( 𝑋 𝑀 𝑍 ) 𝐿 𝑒 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑌 ) )
200 198 199 r19.29a ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )