Metamath Proof Explorer


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 ( 𝜑𝑋 = ( ( 𝐷𝐵 ) / ( 𝐴𝐶 ) ) )