Theorem rrxlinec

Description: The line passing through the two different points X and Y in a generalized real Euclidean space of finite dimension, expressed by its coordinates. Remark: This proof is shorter and requires less distinct variables than the proof using rrxlinesc . (Contributed by AV, 13-Feb-2023)

	Ref	Expression
Hypotheses	rrxlinesc.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	rrxlinesc.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	rrxlinesc.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
Assertion	rrxlinec	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		rrxlinesc.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
2		rrxlinesc.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		rrxlinesc.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
4		eqid	⊢ ( ·𝑠 ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐸 )
5		eqid	⊢ ( +g ‘ 𝐸 ) = ( +g ‘ 𝐸 )
6	1 2 3 4 5	rrxline	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑋 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑌 ) ) } )
7		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8		simplll	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝐼 ∈ Fin )
9		1red	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 1 ∈ ℝ )
10		simpr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
11	9 10	resubcld	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) ∈ ℝ )
12		id	⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
13	12 1 7	rrxbasefi	⊢ ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = ( ℝ ↑m 𝐼 ) )
14	2 13	eqtr4id	⊢ ( 𝐼 ∈ Fin → 𝑃 = ( Base ‘ 𝐸 ) )
15	14	eleq2d	⊢ ( 𝐼 ∈ Fin → ( 𝑋 ∈ 𝑃 ↔ 𝑋 ∈ ( Base ‘ 𝐸 ) ) )
16	15	biimpcd	⊢ ( 𝑋 ∈ 𝑃 → ( 𝐼 ∈ Fin → 𝑋 ∈ ( Base ‘ 𝐸 ) ) )
17	16	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐼 ∈ Fin → 𝑋 ∈ ( Base ‘ 𝐸 ) ) )
18	17	impcom	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐸 ) )
19	18	ad2antrr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑋 ∈ ( Base ‘ 𝐸 ) )
20	14	eleq2d	⊢ ( 𝐼 ∈ Fin → ( 𝑌 ∈ 𝑃 ↔ 𝑌 ∈ ( Base ‘ 𝐸 ) ) )
21	20	biimpcd	⊢ ( 𝑌 ∈ 𝑃 → ( 𝐼 ∈ Fin → 𝑌 ∈ ( Base ‘ 𝐸 ) ) )
22	21	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐼 ∈ Fin → 𝑌 ∈ ( Base ‘ 𝐸 ) ) )
23	22	impcom	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐸 ) )
24	23	ad2antrr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑌 ∈ ( Base ‘ 𝐸 ) )
25	14	adantr	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑃 = ( Base ‘ 𝐸 ) )
26	25	eleq2d	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ ( Base ‘ 𝐸 ) ) )
27	26	biimpa	⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ ( Base ‘ 𝐸 ) )
28	27	adantr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑝 ∈ ( Base ‘ 𝐸 ) )
29	1 7 4 8 11 19 24 28 5 10	rrxplusgvscavalb	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑋 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ) )
30	29	rexbidva	⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑋 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑌 ) ) ↔ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ) )
31	30	rabbidva	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑋 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑌 ) ) } = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } )
32	6 31	eqtrd	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } )