isperp2d

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

	Ref	Expression
Hypotheses	isperp.p	$⊢ P = {Base}_{G}$
	isperp.d	$⊢ \underset{˙}{-} = dist (G)$
	isperp.i	$⊢ I = Itv (G)$
	isperp.l	$⊢ L = {Line}_{𝒢} (G)$
	isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	isperp.a	$⊢ φ \to A \in ran L$
	isperp2.b	$⊢ φ \to B \in ran L$
	isperp2.x	$⊢ φ \to X \in (A \cap B)$
	isperp2d.u	$⊢ φ \to U \in A$
	isperp2d.v	$⊢ φ \to V \in B$
	isperp2d.p	$⊢ φ \to A ⟂_{𝒢} (G) B$
Assertion	isperp2d	$⊢ φ \to ⟨“ U X V ”⟩ \in ∟_{𝒢} (G)$

Proof

Step	Hyp	Ref	Expression
1		isperp.p	$⊢ P = {Base}_{G}$
2		isperp.d	$⊢ \underset{˙}{-} = dist (G)$
3		isperp.i	$⊢ I = Itv (G)$
4		isperp.l	$⊢ L = {Line}_{𝒢} (G)$
5		isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		isperp.a	$⊢ φ \to A \in ran L$
7		isperp2.b	$⊢ φ \to B \in ran L$
8		isperp2.x	$⊢ φ \to X \in (A \cap B)$
9		isperp2d.u	$⊢ φ \to U \in A$
10		isperp2d.v	$⊢ φ \to V \in B$
11		isperp2d.p	$⊢ φ \to A ⟂_{𝒢} (G) B$
12	1 2 3 4 5 6 7 8	isperp2	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$
13	11 12	mpbid	$⊢ φ \to \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)$
14		id	$⊢ u = U \to u = U$
15		eqidd	$⊢ u = U \to X = X$
16		eqidd	$⊢ u = U \to v = v$
17	14 15 16	s3eqd	$⊢ u = U \to ⟨“ u X v ”⟩ = ⟨“ U X v ”⟩$
18	17	eleq1d	$⊢ u = U \to (⟨“ u X v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ U X v ”⟩ \in ∟_{𝒢} (G))$
19		eqidd	$⊢ v = V \to U = U$
20		eqidd	$⊢ v = V \to X = X$
21		id	$⊢ v = V \to v = V$
22	19 20 21	s3eqd	$⊢ v = V \to ⟨“ U X v ”⟩ = ⟨“ U X V ”⟩$
23	22	eleq1d	$⊢ v = V \to (⟨“ U X v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ U X V ”⟩ \in ∟_{𝒢} (G))$
24	18 23	rspc2v	$⊢ (U \in A \land V \in B) \to (\forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G) \to ⟨“ U X V ”⟩ \in ∟_{𝒢} (G))$
25	9 10 24	syl2anc	$⊢ φ \to (\forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G) \to ⟨“ U X V ”⟩ \in ∟_{𝒢} (G))$
26	13 25	mpd	$⊢ φ \to ⟨“ U X V ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem isperp2d

Proof