Theorem line2ylem

Description: Lemma for line2y . This proof is based on counterexamples for the following cases: 1. C =/= 0 : p = (0,0) (LHS of bicondional is false, RHS is true); 2. C = 0 /\ B =/= 0 : p = (1,-A/B) (LHS of bicondional is true, RHS is false); 3. A = B = C = 0 : p = (1,1) (LHS of bicondional is true, RHS is false). (Contributed by AV, 4-Feb-2023)

	Ref	Expression
Hypotheses	line2ylem.i	⊢ 𝐼 = { 1 , 2 }
	line2ylem.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion	line2ylem	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		line2ylem.i	⊢ 𝐼 = { 1 , 2 }
2		line2ylem.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		ianor	⊢ ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) ↔ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) )
4		df-ne	⊢ ( 𝐶 ≠ 0 ↔ ¬ 𝐶 = 0 )
5		0re	⊢ 0 ∈ ℝ
6	1 2	prelrrx2	⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∈ 𝑃 )
7	5 5 6	mp2an	⊢ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∈ 𝑃
8		eqneqall	⊢ ( 𝐶 = 0 → ( 𝐶 ≠ 0 → ¬ 0 = 0 ) )
9	8	com12	⊢ ( 𝐶 ≠ 0 → ( 𝐶 = 0 → ¬ 0 = 0 ) )
10		eqid	⊢ 0 = 0
11	10	pm2.24i	⊢ ( ¬ 0 = 0 → 𝐶 = 0 )
12	9 11	impbid1	⊢ ( 𝐶 ≠ 0 → ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
13	12	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
14		xor3	⊢ ( ¬ ( 𝐶 = 0 ↔ 0 = 0 ) ↔ ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
15	13 14	sylibr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ¬ ( 𝐶 = 0 ↔ 0 = 0 ) )
16		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
17	16	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
18	17	mul01d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 0 ) = 0 )
19		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
20	19	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
21	20	mul01d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 0 ) = 0 )
22	18 21	oveq12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = ( 0 + 0 ) )
23		00id	⊢ ( 0 + 0 ) = 0
24	22 23	eqtrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 0 )
25	24	eqeq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 𝐶 ) )
26		eqcom	⊢ ( 0 = 𝐶 ↔ 𝐶 = 0 )
27	25 26	bitrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 𝐶 = 0 ) )
28	27	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 𝐶 = 0 ) )
29	28	bibi1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ↔ ( 𝐶 = 0 ↔ 0 = 0 ) ) )
30	15 29	mtbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) )
31		fveq1	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) )
32		1ex	⊢ 1 ∈ V
33		c0ex	⊢ 0 ∈ V
34		1ne2	⊢ 1 ≠ 2
35		fvpr1g	⊢ ( ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 0 )
36	32 33 34 35	mp3an	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 0
37	31 36	eqtrdi	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 1 ) = 0 )
38	37	oveq2d	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · 0 ) )
39		fveq1	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) )
40		2ex	⊢ 2 ∈ V
41		fvpr2g	⊢ ( ( 2 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0 )
42	40 33 34 41	mp3an	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0
43	39 42	eqtrdi	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 2 ) = 0 )
44	43	oveq2d	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · 0 ) )
45	38 44	oveq12d	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) )
46	45	eqeq1d	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ) )
47	37	eqeq1d	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( 𝑝 ‘ 1 ) = 0 ↔ 0 = 0 ) )
48	46 47	bibi12d	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) )
49	48	notbid	⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) )
50	49	rspcev	⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
51	7 30 50	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
52	51	expcom	⊢ ( 𝐶 ≠ 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
53	4 52	sylbir	⊢ ( ¬ 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
54		notnotb	⊢ ( 𝐶 = 0 ↔ ¬ ¬ 𝐶 = 0 )
55		ianor	⊢ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ↔ ( ¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0 ) )
56		df-ne	⊢ ( 𝐵 ≠ 0 ↔ ¬ 𝐵 = 0 )
57		1red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 1 ∈ ℝ )
58	16	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐴 ∈ ℝ )
59	58	renegcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → - 𝐴 ∈ ℝ )
60	19	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ∈ ℝ )
61		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ≠ 0 )
62	59 60 61	redivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( - 𝐴 / 𝐵 ) ∈ ℝ )
63	1 2	prelrrx2	⊢ ( ( 1 ∈ ℝ ∧ ( - 𝐴 / 𝐵 ) ∈ ℝ ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ∈ 𝑃 )
64	57 62 63	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ∈ 𝑃 )
65		ax-1ne0	⊢ 1 ≠ 0
66	65	neii	⊢ ¬ 1 = 0
67	10 66	2th	⊢ ( 0 = 0 ↔ ¬ 1 = 0 )
68		xor3	⊢ ( ¬ ( 0 = 0 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ ¬ 1 = 0 ) )
69	67 68	mpbir	⊢ ¬ ( 0 = 0 ↔ 1 = 0 )
70	17	mulridd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 1 ) = 𝐴 )
71	70	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐴 · 1 ) = 𝐴 )
72	17	negcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → - 𝐴 ∈ ℂ )
73	72	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → - 𝐴 ∈ ℂ )
74	20	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ∈ ℂ )
75	73 74 61	divcan2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐵 · ( - 𝐴 / 𝐵 ) ) = - 𝐴 )
76	71 75	oveq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = ( 𝐴 + - 𝐴 ) )
77	17	negidd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + - 𝐴 ) = 0 )
78	77	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐴 + - 𝐴 ) = 0 )
79	76 78	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 0 )
80		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐶 = 0 )
81	79 80	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 0 = 0 ) )
82	81	bibi1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ 1 = 0 ) ) )
83	69 82	mtbiri	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) )
84		fveq1	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 1 ) )
85		fvpr1g	⊢ ( ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 1 ) = 1 )
86	32 32 34 85	mp3an	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 1 ) = 1
87	84 86	eqtrdi	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 1 ) = 1 )
88	87	oveq2d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · 1 ) )
89		fveq1	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 2 ) )
90		ovex	⊢ ( - 𝐴 / 𝐵 ) ∈ V
91		fvpr2g	⊢ ( ( 2 ∈ V ∧ ( - 𝐴 / 𝐵 ) ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 2 ) = ( - 𝐴 / 𝐵 ) )
92	40 90 34 91	mp3an	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 2 ) = ( - 𝐴 / 𝐵 )
93	89 92	eqtrdi	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 2 ) = ( - 𝐴 / 𝐵 ) )
94	93	oveq2d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · ( - 𝐴 / 𝐵 ) ) )
95	88 94	oveq12d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) )
96	95	eqeq1d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ) )
97	87	eqeq1d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( 𝑝 ‘ 1 ) = 0 ↔ 1 = 0 ) )
98	96 97	bibi12d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) )
99	98	notbid	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) )
100	99	rspcev	⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
101	64 83 100	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
102	101	expcom	⊢ ( ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
103	102	ex	⊢ ( 𝐵 ≠ 0 → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
104	56 103	sylbir	⊢ ( ¬ 𝐵 = 0 → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
105		notnotb	⊢ ( 𝐵 = 0 ↔ ¬ ¬ 𝐵 = 0 )
106		nne	⊢ ( ¬ 𝐴 ≠ 0 ↔ 𝐴 = 0 )
107	106	bicomi	⊢ ( 𝐴 = 0 ↔ ¬ 𝐴 ≠ 0 )
108		1re	⊢ 1 ∈ ℝ
109	1 2	prelrrx2	⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 )
110	108 108 109	mp2an	⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃
111		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 · 1 ) = ( 0 · 1 ) )
112	111	adantl	⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐴 · 1 ) = ( 0 · 1 ) )
113		ax-1cn	⊢ 1 ∈ ℂ
114	113	mul02i	⊢ ( 0 · 1 ) = 0
115	112 114	eqtrdi	⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐴 · 1 ) = 0 )
116		oveq1	⊢ ( 𝐵 = 0 → ( 𝐵 · 1 ) = ( 0 · 1 ) )
117	116	adantr	⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐵 · 1 ) = ( 0 · 1 ) )
118	117 114	eqtrdi	⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐵 · 1 ) = 0 )
119	115 118	oveq12d	⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = ( 0 + 0 ) )
120	119 23	eqtrdi	⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 0 )
121		id	⊢ ( 𝐶 = 0 → 𝐶 = 0 )
122	120 121	eqeqan12d	⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 0 = 0 ) )
123	122	bibi1d	⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ 1 = 0 ) ) )
124	69 123	mtbiri	⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) )
125		fveq1	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) )
126		fvpr1g	⊢ ( ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 1 )
127	32 32 34 126	mp3an	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 1
128	125 127	eqtrdi	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 1 ) = 1 )
129	128	oveq2d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · 1 ) )
130		fveq1	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) )
131		fvpr2g	⊢ ( ( 2 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1 )
132	40 32 34 131	mp3an	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1
133	130 132	eqtrdi	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 2 ) = 1 )
134	133	oveq2d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · 1 ) )
135	129 134	oveq12d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) )
136	135	eqeq1d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ) )
137	128	eqeq1d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( 𝑝 ‘ 1 ) = 0 ↔ 1 = 0 ) )
138	136 137	bibi12d	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) )
139	138	notbid	⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) )
140	139	rspcev	⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
141	110 124 140	sylancr	⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
142	141	a1d	⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
143	142	ex	⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
144	105 107 143	syl2anbr	⊢ ( ( ¬ ¬ 𝐵 = 0 ∧ ¬ 𝐴 ≠ 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
145	104 144	jaoi3	⊢ ( ( ¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
146	145	orcoms	⊢ ( ( ¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
147	55 146	sylbi	⊢ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
148	147	com12	⊢ ( 𝐶 = 0 → ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
149	54 148	sylbir	⊢ ( ¬ ¬ 𝐶 = 0 → ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
150	149	imp	⊢ ( ( ¬ ¬ 𝐶 = 0 ∧ ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
151	53 150	jaoi3	⊢ ( ( ¬ 𝐶 = 0 ∨ ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
152	151	orcoms	⊢ ( ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
153	152	com12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
154	3 153	biimtrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
155		rexnal	⊢ ( ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
156	154 155	imbitrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) → ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
157	156	con4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) ) )
158		df-3an	⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ↔ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) )
159	157 158	imbitrrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )