Metamath Proof Explorer

Theorem inagswap

Description: Swap the order of the half lines delimiting the angle. Theorem 11.24 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Hypotheses isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
inagflat.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
inagswap.1 ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
Assertion inagswap ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ )

Proof

Step Hyp Ref Expression
1 isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5 isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 inagflat.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
9 inagswap.1 ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
10 1 2 3 4 5 6 7 8 isinag ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )
11 9 10 mpbid ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
12 11 simpld ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) )
13 12 simp2d ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
14 12 simp1d ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
15 12 simp3d ⊢ ( 𝜑 → 𝑋 ≠ 𝐵 )
16 13 14 15 3jca ⊢ ( 𝜑 → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) )
17 11 simprd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
18 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
19 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
20 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
21 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑥 ∈ 𝑃 )
22 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
23 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) )
24 1 18 2 19 20 21 22 23 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) )
25 24 3expia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) → 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) ) )
26 25 anim1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) → ( 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
27 26 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
28 17 27 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
29 1 2 3 4 7 6 5 8 isinag ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ ↔ ( ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )
30 16 28 29 mpbir2and ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ )