Theorem i2linesi

Description: Solve for the intersection of two lines expressed in Y = MX+B form (note that the lines cannot be vertical). Here we use inference 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, 11-Oct-2018)

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

Proof

Step	Hyp	Ref	Expression
1		i2linesi.1	⊢ 𝐴 ∈ ℂ
2		i2linesi.2	⊢ 𝐵 ∈ ℂ
3		i2linesi.3	⊢ 𝐶 ∈ ℂ
4		i2linesi.4	⊢ 𝐷 ∈ ℂ
5		i2linesi.5	⊢ 𝑋 ∈ ℂ
6		i2linesi.6	⊢ 𝑌 = ( ( 𝐴 · 𝑋 ) + 𝐵 )
7		i2linesi.7	⊢ 𝑌 = ( ( 𝐶 · 𝑋 ) + 𝐷 )
8		i2linesi.8	⊢ ( 𝐴 − 𝐶 ) ≠ 0
9	1 3	subcli	⊢ ( 𝐴 − 𝐶 ) ∈ ℂ
10	3 5	mulcli	⊢ ( 𝐶 · 𝑋 ) ∈ ℂ
11	4 2	subcli	⊢ ( 𝐷 − 𝐵 ) ∈ ℂ
12	1 5	mulcli	⊢ ( 𝐴 · 𝑋 ) ∈ ℂ
13	6 7	eqtr3i	⊢ ( ( 𝐴 · 𝑋 ) + 𝐵 ) = ( ( 𝐶 · 𝑋 ) + 𝐷 )
14	12 2 13	mvlraddi	⊢ ( 𝐴 · 𝑋 ) = ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − 𝐵 )
15	10 4 2 14	assraddsubi	⊢ ( 𝐴 · 𝑋 ) = ( ( 𝐶 · 𝑋 ) + ( 𝐷 − 𝐵 ) )
16	10 11 15	mvrladdi	⊢ ( ( 𝐴 · 𝑋 ) − ( 𝐶 · 𝑋 ) ) = ( 𝐷 − 𝐵 )
17	1 5 3 16	joinlmulsubmuli	⊢ ( ( 𝐴 − 𝐶 ) · 𝑋 ) = ( 𝐷 − 𝐵 )
18	9 5 8 17	mvllmuli	⊢ 𝑋 = ( ( 𝐷 − 𝐵 ) / ( 𝐴 − 𝐶 ) )