Theorem sharhght

Description: Let A B C be a triangle, and let D lie on the line A B . Then (doubled) areas of triangles A D C and C D B relate as lengths of corresponding bases A D and D B . (Contributed by Saveliy Skresanov, 23-Sep-2017)

	Ref	Expression
Hypotheses	sharhght.sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
	sharhght.a	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
	sharhght.b	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 ) )
Assertion	sharhght	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sharhght.sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2		sharhght.a	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3		sharhght.b	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 ) )
4	2	simp3d	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5	2	simp1d	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6	4 5	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ ℂ )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
8	3	simpld	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
9	8 5	subcld	⊢ ( 𝜑 → ( 𝐷 − 𝐴 ) ∈ ℂ )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐴 ) ∈ ℂ )
11	1	sigarim	⊢ ( ( ( 𝐶 − 𝐴 ) ∈ ℂ ∧ ( 𝐷 − 𝐴 ) ∈ ℂ ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
12	7 10 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
13	12	recnd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℂ )
14	13	mul01d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · 0 ) = 0 )
15	2	simp2d	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐵 ∈ ℂ )
17		simpr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐵 = 𝐷 )
18	16 17	subeq0bd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐷 ) = 0 )
19	18	oveq2d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · 0 ) )
20	4 15	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
22	8 15	subcld	⊢ ( 𝜑 → ( 𝐷 − 𝐵 ) ∈ ℂ )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) ∈ ℂ )
24	1	sigarval	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) ) )
25	21 23 24	syl2anc	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) ) )
26	8	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐷 ∈ ℂ )
27	17	eqcomd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐷 = 𝐵 )
28	26 27	subeq0bd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) = 0 )
29	28	oveq2d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) = ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · 0 ) )
30	21	cjcld	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ∗ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
31	30	mul01d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · 0 ) = 0 )
32	29 31	eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) = 0 )
33	32	fveq2d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) ) = ( ℑ ‘ 0 ) )
34		0red	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 0 ∈ ℝ )
35	34	reim0d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ℑ ‘ 0 ) = 0 )
36	25 33 35	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) = 0 )
37	36	oveq1d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) = ( 0 · ( 𝐴 − 𝐷 ) ) )
38	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐴 ∈ ℂ )
39	38 26	subcld	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐴 − 𝐷 ) ∈ ℂ )
40	39	mul02d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 0 · ( 𝐴 − 𝐷 ) ) = 0 )
41	37 40	eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) = 0 )
42	14 19 41	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )
43	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐶 ∈ ℂ )
44	15	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐵 ∈ ℂ )
45	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐴 ∈ ℂ )
46	43 44 45	npncand	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐶 − 𝐴 ) )
47	46	oveq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
48	43 44	subcld	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
49	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐴 ) ∈ ℂ )
50	44 45	subcld	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
51	1	sigaraf	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 − 𝐴 ) ∈ ℂ ) → ( ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
52	48 49 50 51	syl3anc	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
53	47 52	eqtr3d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
54	3	simprd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 )
55	54	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 )
56	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐷 ∈ ℂ )
57	1	sigarperm	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
58	45 44 56 57	syl3anc	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
59	55 58	eqtr3d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 0 = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
60	59	oveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + 0 ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
61	1	sigarim	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐴 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
62	48 49 61	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
63	62	recnd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℂ )
64	63	addridd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + 0 ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
65	53 60 64	3eqtr2d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
66	44 56	negsubdi2d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( 𝐵 − 𝐷 ) = ( 𝐷 − 𝐵 ) )
67	66	eqcomd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) = - ( 𝐵 − 𝐷 ) )
68	67	oveq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) = ( - ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) )
69	44 56	subcld	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐷 ) ∈ ℂ )
70		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ¬ 𝐵 = 𝐷 )
71	70	neqned	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐵 ≠ 𝐷 )
72	44 56 71	subne0d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐷 ) ≠ 0 )
73	69 69 72	divnegd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) = ( - ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) )
74	69 72	dividd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) = 1 )
75	74	negeqd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) = - 1 )
76	68 73 75	3eqtr2d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) = - 1 )
77	76	oveq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐴 − 𝐷 ) ) = ( - 1 · ( 𝐴 − 𝐷 ) ) )
78	45 56	subcld	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐴 − 𝐷 ) ∈ ℂ )
79	78	mulm1d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( - 1 · ( 𝐴 − 𝐷 ) ) = - ( 𝐴 − 𝐷 ) )
80	45 56	negsubdi2d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( 𝐴 − 𝐷 ) = ( 𝐷 − 𝐴 ) )
81	77 79 80	3eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐴 − 𝐷 ) ) = ( 𝐷 − 𝐴 ) )
82	56 44	subcld	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) ∈ ℂ )
83	82 69 78 72	div32d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐴 − 𝐷 ) ) = ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
84	81 83	eqtr3d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐴 ) = ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
85	84	oveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) ) )
86	56 45 44	3jca	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
87	1 86 70 55	sigardiv	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ∈ ℝ )
88	1	sigarls	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ∈ ℝ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
89	48 82 87 88	syl3anc	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
90	65 85 89	3eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
91	90	oveq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) · ( 𝐵 − 𝐷 ) ) )
92	1	sigarim	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℝ )
93	92	recnd	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℂ )
94	48 82 93	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℂ )
95	78 69 72	divcld	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ∈ ℂ )
96	94 95 69	mulassd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐵 − 𝐷 ) ) ) )
97	78 69 72	divcan1d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐵 − 𝐷 ) ) = ( 𝐴 − 𝐷 ) )
98	97	oveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐵 − 𝐷 ) ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )
99	91 96 98	3eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )
100	42 99	pm2.61dan	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )