Theorem line2y

Description: Example for a vertical 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 ) ) ) = 𝐶 }
	line2y.x	⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
	line2y.y	⊢ 𝑌 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ }
Assertion	line2y	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 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		line2y.x	⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
7		line2y.y	⊢ 𝑌 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ }
8	5	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 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 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → 0 ∈ ℝ )
18		simp2r	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → 𝑀 ∈ ℝ )
19	17 18	prssd	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { 0 , 𝑀 } ⊆ ℝ )
20	16 19	fssd	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
21	11 13 15 20	mp3an2i	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
22	1	feq2i	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
23	21 22	sylibr	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
24		reex	⊢ ℝ ∈ V
25		prex	⊢ { 1 , 2 } ∈ V
26	1 25	eqeltri	⊢ 𝐼 ∈ V
27	24 26	elmap	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
28	23 27	sylibr	⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) )
29	28 6 3	3eltr4g	⊢ ( 𝑀 ∈ ℝ → 𝑋 ∈ 𝑃 )
30	29	3ad2ant1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑋 ∈ 𝑃 )
31	12	jctl	⊢ ( 𝑁 ∈ ℝ → ( 0 ∈ V ∧ 𝑁 ∈ ℝ ) )
32	14	a1i	⊢ ( 𝑁 ∈ ℝ → 1 ≠ 2 )
33		fprg	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑁 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : { 1 , 2 } ⟶ { 0 , 𝑁 } )
34	11 31 32 33	mp3an2i	⊢ ( 𝑁 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : { 1 , 2 } ⟶ { 0 , 𝑁 } )
35		0re	⊢ 0 ∈ ℝ
36		prssi	⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → { 0 , 𝑁 } ⊆ ℝ )
37	35 36	mpan	⊢ ( 𝑁 ∈ ℝ → { 0 , 𝑁 } ⊆ ℝ )
38	34 37	fssd	⊢ ( 𝑁 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : { 1 , 2 } ⟶ ℝ )
39	1	feq2i	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : 𝐼 ⟶ ℝ ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : { 1 , 2 } ⟶ ℝ )
40	38 39	sylibr	⊢ ( 𝑁 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : 𝐼 ⟶ ℝ )
41	24 26	pm3.2i	⊢ ( ℝ ∈ V ∧ 𝐼 ∈ V )
42		elmapg	⊢ ( ( ℝ ∈ V ∧ 𝐼 ∈ V ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : 𝐼 ⟶ ℝ ) )
43	41 42	mp1i	⊢ ( 𝑁 ∈ ℝ → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } : 𝐼 ⟶ ℝ ) )
44	40 43	mpbird	⊢ ( 𝑁 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ∈ ( ℝ ↑m 𝐼 ) )
45	44 7 3	3eltr4g	⊢ ( 𝑁 ∈ ℝ → 𝑌 ∈ 𝑃 )
46	45	3ad2ant2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑌 ∈ 𝑃 )
47	6	fveq1i	⊢ ( 𝑋 ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 )
48	9 12 14	3pm3.2i	⊢ ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 )
49		fvpr1g	⊢ ( ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
50	48 49	mp1i	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
51	47 50	eqtrid	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 1 ) = 0 )
52	7	fveq1i	⊢ ( 𝑌 ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ‘ 1 )
53		fvpr1g	⊢ ( ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ‘ 1 ) = 0 )
54	48 53	mp1i	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ‘ 1 ) = 0 )
55	52 54	eqtrid	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑌 ‘ 1 ) = 0 )
56	51 55	eqtr4d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
57		simp3	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑀 ≠ 𝑁 )
58	6	fveq1i	⊢ ( 𝑋 ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 )
59		simp1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑀 ∈ ℝ )
60	14	a1i	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 1 ≠ 2 )
61		fvpr2g	⊢ ( ( 2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
62	10 59 60 61	mp3an2i	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
63	58 62	eqtrid	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 2 ) = 𝑀 )
64	7	fveq1i	⊢ ( 𝑌 ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ‘ 2 )
65		simp2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑁 ∈ ℝ )
66		fvpr2g	⊢ ( ( 2 ∈ V ∧ 𝑁 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ‘ 2 ) = 𝑁 )
67	10 65 60 66	mp3an2i	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ } ‘ 2 ) = 𝑁 )
68	64 67	eqtrid	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑌 ‘ 2 ) = 𝑁 )
69	57 63 68	3netr4d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) )
70	56 69	jca	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )
71	30 46 70	3jca	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) )
72	71	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) )
73	1 2 3 4	rrx2vlinest	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } )
74	72 73	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } )
75	8 74	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } ) )
76	48 49	ax-mp	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0
77	47 76	eqtri	⊢ ( 𝑋 ‘ 1 ) = 0
78	77	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝑋 ‘ 1 ) = 0 )
79	78	eqeq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) ↔ ( 𝑝 ‘ 1 ) = 0 ) )
80	79	rabbidv	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = 0 } )
81	80	eqeq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = 0 } ) )
82		rabbi	⊢ ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = 0 } )
83	1 3	line2ylem	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
84	83	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
85		oveq1	⊢ ( 𝐵 = 0 → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 0 · ( 𝑝 ‘ 2 ) ) )
86	85	3ad2ant2	⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 0 · ( 𝑝 ‘ 2 ) ) )
87	86	oveq2d	⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 0 · ( 𝑝 ‘ 2 ) ) ) )
88		simp3	⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → 𝐶 = 0 )
89	87 88	eqeq12d	⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 0 · ( 𝑝 ‘ 2 ) ) ) = 0 ) )
90	89	ad2antlr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 0 · ( 𝑝 ‘ 2 ) ) ) = 0 ) )
91	1 3	rrx2pyel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
92	91	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℂ )
93	92	mul02d	⊢ ( 𝑝 ∈ 𝑃 → ( 0 · ( 𝑝 ‘ 2 ) ) = 0 )
94	93	adantl	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 · ( 𝑝 ‘ 2 ) ) = 0 )
95	94	oveq2d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 0 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + 0 ) )
96		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
97	96	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
98	97	ad3antrrr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 ∈ ℂ )
99	1 3	rrx2pxel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
100	99	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
101	100	adantl	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
102	98 101	mulcld	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
103	102	addridd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + 0 ) = ( 𝐴 · ( 𝑝 ‘ 1 ) ) )
104	95 103	eqtrd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 0 · ( 𝑝 ‘ 2 ) ) ) = ( 𝐴 · ( 𝑝 ‘ 1 ) ) )
105	104	eqeq1d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 0 · ( 𝑝 ‘ 2 ) ) ) = 0 ↔ ( 𝐴 · ( 𝑝 ‘ 1 ) ) = 0 ) )
106	98 101	mul0ord	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) = 0 ↔ ( 𝐴 = 0 ∨ ( 𝑝 ‘ 1 ) = 0 ) ) )
107		eqneqall	⊢ ( 𝐴 = 0 → ( 𝐴 ≠ 0 → ( 𝑝 ‘ 1 ) = 0 ) )
108	107	com12	⊢ ( 𝐴 ≠ 0 → ( 𝐴 = 0 → ( 𝑝 ‘ 1 ) = 0 ) )
109	108	3ad2ant1	⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( 𝐴 = 0 → ( 𝑝 ‘ 1 ) = 0 ) )
110	109	ad2antlr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 = 0 → ( 𝑝 ‘ 1 ) = 0 ) )
111		idd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) = 0 → ( 𝑝 ‘ 1 ) = 0 ) )
112	110 111	jaod	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 = 0 ∨ ( 𝑝 ‘ 1 ) = 0 ) → ( 𝑝 ‘ 1 ) = 0 ) )
113		olc	⊢ ( ( 𝑝 ‘ 1 ) = 0 → ( 𝐴 = 0 ∨ ( 𝑝 ‘ 1 ) = 0 ) )
114	112 113	impbid1	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 = 0 ∨ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( 𝑝 ‘ 1 ) = 0 ) )
115	106 114	bitrd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) = 0 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
116	90 105 115	3bitrd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
117	116	ralrimiva	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
118	117	ex	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
119	84 118	impbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
120	82 119	bitr3id	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = 0 } ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
121	75 81 120	3bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )