Theorem i2linesd

Description: Solve for the intersection of two lines expressed in Y = MX+B form (note that the lines cannot be vertical). Here we use deduction form. We just solve for X, since Y can be trivially found by using X. This is an example of how to use the algebra helpers. Notice that because this proof uses algebra helpers, the main steps of the proof are higher level and easier to follow by a human reader. (Contributed by David A. Wheeler, 15-Oct-2018)

	Ref	Expression
Hypotheses	i2linesd.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	i2linesd.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	i2linesd.3	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	i2linesd.4	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	i2linesd.5	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	i2linesd.6	⊢ ( 𝜑 → 𝑌 = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
	i2linesd.7	⊢ ( 𝜑 → 𝑌 = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
	i2linesd.8	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ≠ 0 )
Assertion	i2linesd	⊢ ( 𝜑 → 𝑋 = ( ( 𝐷 − 𝐵 ) / ( 𝐴 − 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		i2linesd.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		i2linesd.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		i2linesd.3	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		i2linesd.4	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		i2linesd.5	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
6		i2linesd.6	⊢ ( 𝜑 → 𝑌 = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
7		i2linesd.7	⊢ ( 𝜑 → 𝑌 = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
8		i2linesd.8	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ≠ 0 )
9	1 3	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
10	3 5	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ ℂ )
11	4 2	subcld	⊢ ( 𝜑 → ( 𝐷 − 𝐵 ) ∈ ℂ )
12	1 5	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ℂ )
13	6 7	eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + 𝐵 ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
14	12 2 13	mvlraddd	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) = ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − 𝐵 ) )
15	10 4 2 14	assraddsubd	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) = ( ( 𝐶 · 𝑋 ) + ( 𝐷 − 𝐵 ) ) )
16	10 11 15	mvrladdd	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) − ( 𝐶 · 𝑋 ) ) = ( 𝐷 − 𝐵 ) )
17	1 5 3 16	joinlmulsubmuld	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) · 𝑋 ) = ( 𝐷 − 𝐵 ) )
18	9 5 8 17	mvllmuld	⊢ ( 𝜑 → 𝑋 = ( ( 𝐷 − 𝐵 ) / ( 𝐴 − 𝐶 ) ) )