Theorem line2x

Description: Example for a horizontal line G passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023)

	Ref	Expression
Hypotheses	line2.i	⊢ 𝐼 = { 1 , 2 }
	line2.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	line2.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	line2.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
	line2.g	⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
	line2x.x	⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
	line2x.y	⊢ 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ }
Assertion	line2x	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		line2.i	⊢ 𝐼 = { 1 , 2 }
2		line2.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		line2.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		line2.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
5		line2.g	⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
6		line2x.x	⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
7		line2x.y	⊢ 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ }
8	5	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
9		1ex	⊢ 1 ∈ V
10		2ex	⊢ 2 ∈ V
11	9 10	pm3.2i	⊢ ( 1 ∈ V ∧ 2 ∈ V )
12		c0ex	⊢ 0 ∈ V
13	12	jctl	⊢ ( 𝑀 ∈ ℝ → ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) )
14		1ne2	⊢ 1 ≠ 2
15	14	a1i	⊢ ( 𝑀 ∈ ℝ → 1 ≠ 2 )
16		fprg	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ { 0 , 𝑀 } )
17		0red	⊢ ( ( 1 ∈ V ∧ 2 ∈ V ) → 0 ∈ ℝ )
18		simpr	⊢ ( ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) → 𝑀 ∈ ℝ )
19	17 18	anim12i	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ) → ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
20	19	3adant3	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
21		prssi	⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → { 0 , 𝑀 } ⊆ ℝ )
22	20 21	syl	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { 0 , 𝑀 } ⊆ ℝ )
23	16 22	fssd	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
24	11 13 15 23	mp3an2i	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
25	1	feq2i	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
26	24 25	sylibr	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
27		reex	⊢ ℝ ∈ V
28		prex	⊢ { 1 , 2 } ∈ V
29	1 28	eqeltri	⊢ 𝐼 ∈ V
30	27 29	elmap	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
31	26 30	sylibr	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) )
32	31 6 3	3eltr4g	⊢ ( 𝑀 ∈ ℝ → 𝑋 ∈ 𝑃 )
33	9	jctl	⊢ ( 𝑀 ∈ ℝ → ( 1 ∈ V ∧ 𝑀 ∈ ℝ ) )
34		fprg	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 1 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ { 1 , 𝑀 } )
35	11 33 15 34	mp3an2i	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ { 1 , 𝑀 } )
36		1re	⊢ 1 ∈ ℝ
37		prssi	⊢ ( ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → { 1 , 𝑀 } ⊆ ℝ )
38	36 37	mpan	⊢ ( 𝑀 ∈ ℝ → { 1 , 𝑀 } ⊆ ℝ )
39	35 38	fssd	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
40	1	feq2i	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
41	39 40	sylibr	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
42	27 29	pm3.2i	⊢ ( ℝ ∈ V ∧ 𝐼 ∈ V )
43		elmapg	⊢ ( ( ℝ ∈ V ∧ 𝐼 ∈ V ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ) )
44	42 43	mp1i	⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ) )
45	41 44	mpbird	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) )
46	45 7 3	3eltr4g	⊢ ( 𝑀 ∈ ℝ → 𝑌 ∈ 𝑃 )
47		opex	⊢ ⟨ 1 , 0 ⟩ ∈ V
48		opex	⊢ ⟨ 2 , 𝑀 ⟩ ∈ V
49	47 48	pm3.2i	⊢ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V )
50		opex	⊢ ⟨ 1 , 1 ⟩ ∈ V
51	50 48	pm3.2i	⊢ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V )
52	49 51	pm3.2i	⊢ ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) )
53	14	orci	⊢ ( 1 ≠ 2 ∨ 0 ≠ 𝑀 )
54	9 12	opthne	⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ↔ ( 1 ≠ 2 ∨ 0 ≠ 𝑀 ) )
55	53 54	mpbir	⊢ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩
56	55	a1i	⊢ ( 𝑀 ∈ ℝ → ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ )
57		0ne1	⊢ 0 ≠ 1
58	57	olci	⊢ ( 1 ≠ 1 ∨ 0 ≠ 1 )
59	9 12	opthne	⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ↔ ( 1 ≠ 1 ∨ 0 ≠ 1 ) )
60	58 59	mpbir	⊢ ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩
61	56 60	jctil	⊢ ( 𝑀 ∈ ℝ → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) )
62	61	orcd	⊢ ( 𝑀 ∈ ℝ → ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ∨ ( ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ) )
63		prneimg	⊢ ( ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) ) → ( ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ∨ ( ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ) )
64	52 62 63	mpsyl	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } )
65	64 6 7	3netr4g	⊢ ( 𝑀 ∈ ℝ → 𝑋 ≠ 𝑌 )
66	32 46 65	3jca	⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
67	66	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
68		eqid	⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
69		eqid	⊢ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
70		eqid	⊢ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
71	1 2 3 4 68 69 70	rrx2linest	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } )
72	67 71	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } )
73	8 72	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } ) )
74		rabbi	⊢ ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } )
75	7	fveq1i	⊢ ( 𝑌 ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 )
76	9 9 14	3pm3.2i	⊢ ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 )
77		fvpr1g	⊢ ( ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 1 )
78	76 77	mp1i	⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 1 )
79	75 78	eqtrid	⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 1 ) = 1 )
80	6	fveq1i	⊢ ( 𝑋 ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 )
81	9 12 14	3pm3.2i	⊢ ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 )
82		fvpr1g	⊢ ( ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
83	81 82	mp1i	⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
84	80 83	eqtrid	⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 1 ) = 0 )
85	79 84	oveq12d	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( 1 − 0 ) )
86		1m0e1	⊢ ( 1 − 0 ) = 1
87	85 86	eqtrdi	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 1 )
88	87	oveq1d	⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( 1 · ( 𝑝 ‘ 2 ) ) )
89	7	fveq1i	⊢ ( 𝑌 ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 )
90		fvpr2g	⊢ ( ( 2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
91	10 14 90	mp3an13	⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
92	89 91	eqtrid	⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 2 ) = 𝑀 )
93	6	fveq1i	⊢ ( 𝑋 ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 )
94		fvpr2g	⊢ ( ( 2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
95	10 14 94	mp3an13	⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
96	93 95	eqtrid	⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 2 ) = 𝑀 )
97	92 96	oveq12d	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( 𝑀 − 𝑀 ) )
98		recn	⊢ ( 𝑀 ∈ ℝ → 𝑀 ∈ ℂ )
99	98	subidd	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 𝑀 ) = 0 )
100	97 99	eqtrd	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 )
101	100	oveq1d	⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
102	9 9 15 77	mp3an12i	⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 1 )
103	75 102	eqtrid	⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 1 ) = 1 )
104	96 103	oveq12d	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) = ( 𝑀 · 1 ) )
105		ax-1rid	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 · 1 ) = 𝑀 )
106	104 105	eqtrd	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) = 𝑀 )
107	9 12 15 82	mp3an12i	⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
108	80 107	eqtrid	⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 1 ) = 0 )
109	108 92	oveq12d	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) = ( 0 · 𝑀 ) )
110	98	mul02d	⊢ ( 𝑀 ∈ ℝ → ( 0 · 𝑀 ) = 0 )
111	109 110	eqtrd	⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) = 0 )
112	106 111	oveq12d	⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( 𝑀 − 0 ) )
113	98	subid1d	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 0 ) = 𝑀 )
114	112 113	eqtrd	⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = 𝑀 )
115	101 114	oveq12d	⊢ ( 𝑀 ∈ ℝ → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) )
116	88 115	eqeq12d	⊢ ( 𝑀 ∈ ℝ → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 1 · ( 𝑝 ‘ 2 ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) ) )
117	116	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 1 · ( 𝑝 ‘ 2 ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) ) )
118	1 3	rrx2pyel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
119	118	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℂ )
120	119	mullidd	⊢ ( 𝑝 ∈ 𝑃 → ( 1 · ( 𝑝 ‘ 2 ) ) = ( 𝑝 ‘ 2 ) )
121	1 3	rrx2pxel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
122	121	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
123	122	mul02d	⊢ ( 𝑝 ∈ 𝑃 → ( 0 · ( 𝑝 ‘ 1 ) ) = 0 )
124	123	oveq1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) = ( 0 + 𝑀 ) )
125	120 124	eqeq12d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 1 · ( 𝑝 ‘ 2 ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) )
126	117 125	sylan9bb	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) )
127	126	bibi2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ) )
128	127	ralbidva	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ) )
129	98	addlidd	⊢ ( 𝑀 ∈ ℝ → ( 0 + 𝑀 ) = 𝑀 )
130	129	adantr	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( 0 + 𝑀 ) = 𝑀 )
131	130	eqeq2d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) )
132	131	bibi2d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ↔ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
133	132	ralbidva	⊢ ( 𝑀 ∈ ℝ → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
134	133	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
135	1 2 3 4 5 6 7	line2xlem	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) → ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
136		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
137	136	adantr	⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
138	137	ad2antlr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
139	123	adantl	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 · ( 𝑝 ‘ 1 ) ) = 0 )
140	138 139	eqtrd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = 0 )
141	140	oveq1d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( 0 + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) )
142		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
143	142	adantr	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
144	143	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
145	144	ad3antrrr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℂ )
146	119	adantl	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℂ )
147	145 146	mulcld	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℂ )
148	147	addlidd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) )
149	141 148	eqtrd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) )
150	149	eqeq1d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = 𝐶 ) )
151		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
152	151	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
153	152	ad3antrrr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℂ )
154		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℝ )
155	154	recnd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
156	155	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
157	156	ad3antrrr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℂ )
158		simp2r	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ≠ 0 )
159	158	ad3antrrr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ≠ 0 )
160	153 157 146 159	divmuld	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐶 / 𝐵 ) = ( 𝑝 ‘ 2 ) ↔ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = 𝐶 ) )
161		simpr	⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → 𝑀 = ( 𝐶 / 𝐵 ) )
162	161	eqcomd	⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ( 𝐶 / 𝐵 ) = 𝑀 )
163	162	ad2antlr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐶 / 𝐵 ) = 𝑀 )
164	163	eqeq1d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐶 / 𝐵 ) = ( 𝑝 ‘ 2 ) ↔ 𝑀 = ( 𝑝 ‘ 2 ) ) )
165	150 160 164	3bitr2d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ 𝑀 = ( 𝑝 ‘ 2 ) ) )
166		eqcom	⊢ ( 𝑀 = ( 𝑝 ‘ 2 ) ↔ ( 𝑝 ‘ 2 ) = 𝑀 )
167	165 166	bitrdi	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) )
168	167	ralrimiva	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) )
169	168	ex	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
170	135 169	impbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
171	128 134 170	3bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
172	74 171	bitr3id	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
173	73 172	bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )