israg

Description: Property for 3 points A, B, C to form a right angle. Definition 8.1 of Schwabhauser p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019)

	Ref	Expression
Hypotheses	israg.p	$⊢ P = {Base}_{G}$
	israg.d	$⊢ \underset{˙}{-} = dist (G)$
	israg.i	$⊢ I = Itv (G)$
	israg.l	$⊢ L = {Line}_{𝒢} (G)$
	israg.s	$⊢ S = {pInv}_{𝒢} (G)$
	israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	israg.a	$⊢ φ \to A \in P$
	israg.b	$⊢ φ \to B \in P$
	israg.c	$⊢ φ \to C \in P$
Assertion	israg	$⊢ φ \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C))$

Proof

Step	Hyp	Ref	Expression
1		israg.p	$⊢ P = {Base}_{G}$
2		israg.d	$⊢ \underset{˙}{-} = dist (G)$
3		israg.i	$⊢ I = Itv (G)$
4		israg.l	$⊢ L = {Line}_{𝒢} (G)$
5		israg.s	$⊢ S = {pInv}_{𝒢} (G)$
6		israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		israg.a	$⊢ φ \to A \in P$
8		israg.b	$⊢ φ \to B \in P$
9		israg.c	$⊢ φ \to C \in P$
10	7 8 9	s3cld	$⊢ φ \to ⟨“ A B C ”⟩ \in Word P$
11		fveqeq2	$⊢ w = ⟨“ A B C ”⟩ \to (\|w\| = 3 \leftrightarrow \|⟨“ A B C ”⟩\| = 3)$
12		fveq1	$⊢ w = ⟨“ A B C ”⟩ \to w (0) = ⟨“ A B C ”⟩ (0)$
13		fveq1	$⊢ w = ⟨“ A B C ”⟩ \to w (2) = ⟨“ A B C ”⟩ (2)$
14	12 13	oveq12d	$⊢ w = ⟨“ A B C ”⟩ \to w (0) \underset{˙}{-} w (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2)$
15		fveq1	$⊢ w = ⟨“ A B C ”⟩ \to w (1) = ⟨“ A B C ”⟩ (1)$
16	15	fveq2d	$⊢ w = ⟨“ A B C ”⟩ \to S (w (1)) = S (⟨“ A B C ”⟩ (1))$
17	16 13	fveq12d	$⊢ w = ⟨“ A B C ”⟩ \to S (w (1)) (w (2)) = S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))$
18	12 17	oveq12d	$⊢ w = ⟨“ A B C ”⟩ \to w (0) \underset{˙}{-} S (w (1)) (w (2)) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))$
19	14 18	eqeq12d	$⊢ w = ⟨“ A B C ”⟩ \to (w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)) \leftrightarrow ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2)))$
20	11 19	anbi12d	$⊢ w = ⟨“ A B C ”⟩ \to ((\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2))) \leftrightarrow (\|⟨“ A B C ”⟩\| = 3 \land ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))))$
21	20	elrab3	$⊢ ⟨“ A B C ”⟩ \in Word P \to (⟨“ A B C ”⟩ \in \{w \in Word P \| (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))\} \leftrightarrow (\|⟨“ A B C ”⟩\| = 3 \land ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))))$
22	10 21	syl	$⊢ φ \to (⟨“ A B C ”⟩ \in \{w \in Word P \| (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))\} \leftrightarrow (\|⟨“ A B C ”⟩\| = 3 \land ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))))$
23		df-rag	$⊢ ∟_{𝒢} = (g \in V ⟼ \{w \in Word {Base}_{g} \| (\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))\})$
24		simpr	$⊢ (φ \land g = G) \to g = G$
25	24	fveq2d	$⊢ (φ \land g = G) \to {Base}_{g} = {Base}_{G}$
26	25 1	eqtr4di	$⊢ (φ \land g = G) \to {Base}_{g} = P$
27		wrdeq	$⊢ {Base}_{g} = P \to Word {Base}_{g} = Word P$
28	26 27	syl	$⊢ (φ \land g = G) \to Word {Base}_{g} = Word P$
29	24	fveq2d	$⊢ (φ \land g = G) \to dist (g) = dist (G)$
30	29 2	eqtr4di	$⊢ (φ \land g = G) \to dist (g) = \underset{˙}{-}$
31	30	oveqd	$⊢ (φ \land g = G) \to w (0) dist (g) w (2) = w (0) \underset{˙}{-} w (2)$
32		eqidd	$⊢ (φ \land g = G) \to w (0) = w (0)$
33	24	fveq2d	$⊢ (φ \land g = G) \to {pInv}_{𝒢} (g) = {pInv}_{𝒢} (G)$
34	33 5	eqtr4di	$⊢ (φ \land g = G) \to {pInv}_{𝒢} (g) = S$
35	34	fveq1d	$⊢ (φ \land g = G) \to {pInv}_{𝒢} (g) (w (1)) = S (w (1))$
36	35	fveq1d	$⊢ (φ \land g = G) \to {pInv}_{𝒢} (g) (w (1)) (w (2)) = S (w (1)) (w (2))$
37	30 32 36	oveq123d	$⊢ (φ \land g = G) \to w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)) = w (0) \underset{˙}{-} S (w (1)) (w (2))$
38	31 37	eqeq12d	$⊢ (φ \land g = G) \to (w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)) \leftrightarrow w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))$
39	38	anbi2d	$⊢ (φ \land g = G) \to ((\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2))) \leftrightarrow (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2))))$
40	28 39	rabeqbidv	$⊢ (φ \land g = G) \to \{w \in Word {Base}_{g} \| (\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))\} = \{w \in Word P \| (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))\}$
41	6	elexd	$⊢ φ \to G \in V$
42	1	fvexi	$⊢ P \in V$
43	42	wrdexi	$⊢ Word P \in V$
44	43	rabex	$⊢ \{w \in Word P \| (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))\} \in V$
45	44	a1i	$⊢ φ \to \{w \in Word P \| (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))\} \in V$
46	23 40 41 45	fvmptd2	$⊢ φ \to ∟_{𝒢} (G) = \{w \in Word P \| (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))\}$
47	46	eleq2d	$⊢ φ \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ A B C ”⟩ \in \{w \in Word P \| (\|w\| = 3 \land w (0) \underset{˙}{-} w (2) = w (0) \underset{˙}{-} S (w (1)) (w (2)))\})$
48		s3fv0	$⊢ A \in P \to ⟨“ A B C ”⟩ (0) = A$
49	7 48	syl	$⊢ φ \to ⟨“ A B C ”⟩ (0) = A$
50	49	eqcomd	$⊢ φ \to A = ⟨“ A B C ”⟩ (0)$
51		s3fv2	$⊢ C \in P \to ⟨“ A B C ”⟩ (2) = C$
52	9 51	syl	$⊢ φ \to ⟨“ A B C ”⟩ (2) = C$
53	52	eqcomd	$⊢ φ \to C = ⟨“ A B C ”⟩ (2)$
54	50 53	oveq12d	$⊢ φ \to A \underset{˙}{-} C = ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2)$
55		s3fv1	$⊢ B \in P \to ⟨“ A B C ”⟩ (1) = B$
56	8 55	syl	$⊢ φ \to ⟨“ A B C ”⟩ (1) = B$
57	56	eqcomd	$⊢ φ \to B = ⟨“ A B C ”⟩ (1)$
58	57	fveq2d	$⊢ φ \to S (B) = S (⟨“ A B C ”⟩ (1))$
59	58 53	fveq12d	$⊢ φ \to S (B) (C) = S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))$
60	50 59	oveq12d	$⊢ φ \to A \underset{˙}{-} S (B) (C) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))$
61	54 60	eqeq12d	$⊢ φ \to (A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C) \leftrightarrow ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2)))$
62		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
63	62	a1i	$⊢ φ \to \|⟨“ A B C ”⟩\| = 3$
64	63	biantrurd	$⊢ φ \to (⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2)) \leftrightarrow (\|⟨“ A B C ”⟩\| = 3 \land ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))))$
65	61 64	bitrd	$⊢ φ \to (A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C) \leftrightarrow (\|⟨“ A B C ”⟩\| = 3 \land ⟨“ A B C ”⟩ (0) \underset{˙}{-} ⟨“ A B C ”⟩ (2) = ⟨“ A B C ”⟩ (0) \underset{˙}{-} S (⟨“ A B C ”⟩ (1)) (⟨“ A B C ”⟩ (2))))$
66	22 47 65	3bitr4d	$⊢ φ \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C))$

Metamath Proof Explorer

Theorem israg

Proof