Metamath Proof Explorer

Theorem cgrainag

Description: Target-side in-angle transport: if W lies inside angle <" D E F "> and that angle is congruent to <" X Y Z "> , then some point inside <" X Y Z "> makes <" X Y v "> congruent to the sub-angle <" D E W "> . The geometric core of leawittrg . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses cgrainag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
cgrainag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
cgrainag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
cgrainag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
cgrainag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
cgrainag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
cgrainag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
cgrainag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
cgrainag.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
cgrainag.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
cgrainag.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
cgrainag.in ⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
cgrainag.cgb ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
Assertion cgrainag ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 cgrainag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 cgrainag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 cgrainag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 cgrainag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 cgrainag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6 cgrainag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7 cgrainag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
8 cgrainag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9 cgrainag.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10 cgrainag.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
11 cgrainag.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
12 cgrainag.in ⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
13 cgrainag.cgb ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
14 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐺 ∈ TarskiG )
15 14 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐺 ∈ TarskiG )
16 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐷 ∈ 𝑃 )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐷 ∈ 𝑃 )
18 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐸 ∈ 𝑃 )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐸 ∈ 𝑃 )
20 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐹 ∈ 𝑃 )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐹 ∈ 𝑃 )
22 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑊 ∈ 𝑃 )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑊 ∈ 𝑃 )
24 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑋 ∈ 𝑃 )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑋 ∈ 𝑃 )
26 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑌 ∈ 𝑃 )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑌 ∈ 𝑃 )
28 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑍 ∈ 𝑃 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑍 ∈ 𝑃 )
30 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
32 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 )
33 1 2 3 15 17 19 21 23 25 27 29 31 32 inagcgrasubhl ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
34 14 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝐺 ∈ TarskiG )
35 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝐷 ∈ 𝑃 )
36 18 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝐸 ∈ 𝑃 )
37 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝐹 ∈ 𝑃 )
38 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝑊 ∈ 𝑃 )
39 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝑋 ∈ 𝑃 )
40 26 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝑌 ∈ 𝑃 )
41 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝑍 ∈ 𝑃 )
42 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
44 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
45 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
46 1 2 3 34 35 36 37 38 39 40 41 43 44 45 inagcgrasubbtwn ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
47 simpl ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) )
48 47 22 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → 𝑊 ∈ 𝑃 )
49 47 16 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → 𝐷 ∈ 𝑃 )
50 47 18 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → 𝐸 ∈ 𝑃 )
51 47 14 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → 𝐺 ∈ TarskiG )
52 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 )
53 1 2 3 48 49 50 51 52 hlcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 )
54 53 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ) → ( 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ∨ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) )
55 45 olcd ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) ∧ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) → ( 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ∨ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) )
56 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
57 simpr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) )
58 1 2 3 11 5 6 7 4 12 inagne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
59 58 neneqd ⊢ ( 𝜑 → ¬ 𝐷 = 𝐸 )
60 59 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ¬ 𝐷 = 𝐸 )
61 orel2 ⊢ ( ¬ 𝐷 = 𝐸 → ( ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) → 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ) )
62 60 61 syl ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ( ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) → 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ) )
63 57 62 mpd ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) )
64 1 2 3 16 18 22 14 16 56 63 lnhl ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ( 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐷 ∨ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) )
65 54 55 64 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ( 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 ∨ 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) ) )
66 33 46 65 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
67 4 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐺 ∈ TarskiG )
68 5 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐷 ∈ 𝑃 )
69 6 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐸 ∈ 𝑃 )
70 7 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐹 ∈ 𝑃 )
71 11 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑊 ∈ 𝑃 )
72 8 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑋 ∈ 𝑃 )
73 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑌 ∈ 𝑃 )
74 10 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑍 ∈ 𝑃 )
75 13 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
76 12 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
77 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) )
78 1 2 3 67 68 69 70 71 72 73 74 75 56 76 77 inagcgratrgn ⊢ ( ( 𝜑 ∧ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
79 exmid ⊢ ( ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ∨ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) )
80 79 a1i ⊢ ( 𝜑 → ( ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ∨ ¬ ( 𝑊 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐷 = 𝐸 ) ) )
81 66 78 80 mpjaodan ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )