Theorem isperp2d

Description: One direction of isperp2 . (Contributed by Thierry Arnoux, 10-Nov-2019)

	Ref	Expression
Hypotheses	isperp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	isperp.d	⊢ − = ( dist ‘ 𝐺 )
	isperp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	isperp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	isperp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	isperp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	isperp2.b	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
	isperp2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
	isperp2d.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
	isperp2d.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
	isperp2d.p	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
Assertion	isperp2d	⊢ ( 𝜑 → ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		isperp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		isperp.d	⊢ − = ( dist ‘ 𝐺 )
3		isperp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		isperp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		isperp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		isperp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7		isperp2.b	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
8		isperp2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
9		isperp2d.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
10		isperp2d.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
11		isperp2d.p	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
12	1 2 3 4 5 6 7 8	isperp2	⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
13	11 12	mpbid	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
14		id	⊢ ( 𝑢 = 𝑈 → 𝑢 = 𝑈 )
15		eqidd	⊢ ( 𝑢 = 𝑈 → 𝑋 = 𝑋 )
16		eqidd	⊢ ( 𝑢 = 𝑈 → 𝑣 = 𝑣 )
17	14 15 16	s3eqd	⊢ ( 𝑢 = 𝑈 → ⟨“ 𝑢 𝑋 𝑣 ”⟩ = ⟨“ 𝑈 𝑋 𝑣 ”⟩ )
18	17	eleq1d	⊢ ( 𝑢 = 𝑈 → ( ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑈 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
19		eqidd	⊢ ( 𝑣 = 𝑉 → 𝑈 = 𝑈 )
20		eqidd	⊢ ( 𝑣 = 𝑉 → 𝑋 = 𝑋 )
21		id	⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 )
22	19 20 21	s3eqd	⊢ ( 𝑣 = 𝑉 → ⟨“ 𝑈 𝑋 𝑣 ”⟩ = ⟨“ 𝑈 𝑋 𝑉 ”⟩ )
23	22	eleq1d	⊢ ( 𝑣 = 𝑉 → ( ⟨“ 𝑈 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
24	18 23	rspc2v	⊢ ( ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) → ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
25	9 10 24	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) → ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
26	13 25	mpd	⊢ ( 𝜑 → ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )