Metamath Proof Explorer


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 A
i2linesi.2 B
i2linesi.3 C
i2linesi.4 D
i2linesi.5 X
i2linesi.6 Y = A X + B
i2linesi.7 Y = C X + D
i2linesi.8 A C 0
Assertion i2linesi X = D B A C

Proof

Step Hyp Ref Expression
1 i2linesi.1 A
2 i2linesi.2 B
3 i2linesi.3 C
4 i2linesi.4 D
5 i2linesi.5 X
6 i2linesi.6 Y = A X + B
7 i2linesi.7 Y = C X + D
8 i2linesi.8 A C 0
9 1 3 subcli A C
10 3 5 mulcli C X
11 4 2 subcli D B
12 1 5 mulcli A X
13 6 7 eqtr3i A X + B = C X + D
14 12 2 13 mvlraddi A X = C X + D - B
15 10 4 2 14 assraddsubi A X = C X + D - B
16 10 11 15 mvrladdi A X C X = D B
17 1 5 3 16 joinlmulsubmuli A C X = D B
18 9 5 8 17 mvllmuli X = D B A C