This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cply1coe0bi

Description: A polynomial is constant (i.e. a "lifted scalar") iff all but the first coefficient are zero. (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses cply1coe0.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
cply1coe0.0 ⊢ 0 = ( 0g ‘ 𝑅 )
cply1coe0.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cply1coe0.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
cply1coe0.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion cply1coe0bi ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐾 𝑀 = ( 𝐴 ‘ 𝑠 ) ↔ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 cply1coe0.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 cply1coe0.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 cply1coe0.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cply1coe0.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 cply1coe0.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
6 1 2 3 4 5 cply1coe0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝐾 ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑠 ) ) ‘ 𝑛 ) = 0 )
7 6 ad4ant13 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐾 ) ∧ 𝑀 = ( 𝐴 ‘ 𝑠 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑠 ) ) ‘ 𝑛 ) = 0 )
8 fveq2 ⊢ ( 𝑀 = ( 𝐴 ‘ 𝑠 ) → ( coe1 ‘ 𝑀 ) = ( coe1 ‘ ( 𝐴 ‘ 𝑠 ) ) )
9 8 fveq1d ⊢ ( 𝑀 = ( 𝐴 ‘ 𝑠 ) → ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝑠 ) ) ‘ 𝑛 ) )
10 9 eqeq1d ⊢ ( 𝑀 = ( 𝐴 ‘ 𝑠 ) → ( ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ↔ ( ( coe1 ‘ ( 𝐴 ‘ 𝑠 ) ) ‘ 𝑛 ) = 0 ) )
11 10 ralbidv ⊢ ( 𝑀 = ( 𝐴 ‘ 𝑠 ) → ( ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ↔ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑠 ) ) ‘ 𝑛 ) = 0 ) )
12 11 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐾 ) ∧ 𝑀 = ( 𝐴 ‘ 𝑠 ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ↔ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑠 ) ) ‘ 𝑛 ) = 0 ) )
13 7 12 mpbird ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐾 ) ∧ 𝑀 = ( 𝐴 ‘ 𝑠 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 )
14 13 rexlimdva2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐾 𝑀 = ( 𝐴 ‘ 𝑠 ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) )
15 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
16 0nn0 ⊢ 0 ∈ ℕ0
17 eqid ⊢ ( coe1 ‘ 𝑀 ) = ( coe1 ‘ 𝑀 )
18 17 4 3 1 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ 𝐾 )
19 15 16 18 sylancl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ 𝐾 )
20 19 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ 𝐾 )
21 fveq2 ⊢ ( 𝑠 = ( ( coe1 ‘ 𝑀 ) ‘ 0 ) → ( 𝐴 ‘ 𝑠 ) = ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) )
22 21 eqeq2d ⊢ ( 𝑠 = ( ( coe1 ‘ 𝑀 ) ‘ 0 ) → ( 𝑀 = ( 𝐴 ‘ 𝑠 ) ↔ 𝑀 = ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) )
23 22 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) ∧ 𝑠 = ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) → ( 𝑀 = ( 𝐴 ‘ 𝑠 ) ↔ 𝑀 = ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) )
24 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
25 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
26 3 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
27 3 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
28 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
29 5 25 26 27 28 4 asclf ⊢ ( 𝑅 ∈ Ring → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 )
30 29 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 )
31 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32 17 4 3 31 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
33 15 16 32 sylancl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
34 3 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
35 34 eqcomd ⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
36 35 fveq2d ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
37 36 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
38 33 37 eleqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
39 30 38 ffvelcdmd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ∈ 𝐵 )
40 24 15 39 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ∈ 𝐵 ) )
41 40 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ∈ 𝐵 ) )
42 simpr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 )
43 3 5 1 2 coe1scl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( coe1 ‘ 𝑀 ) ‘ 0 ) , 0 ) ) )
44 19 43 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( coe1 ‘ 𝑀 ) ‘ 0 ) , 0 ) ) )
45 44 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( coe1 ‘ 𝑀 ) ‘ 0 ) , 0 ) ) )
46 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
47 46 neneqd ⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 )
48 47 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ¬ 𝑛 = 0 )
49 48 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ¬ 𝑛 = 0 )
50 eqeq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 = 0 ↔ 𝑛 = 0 ) )
51 50 notbid ⊢ ( 𝑘 = 𝑛 → ( ¬ 𝑘 = 0 ↔ ¬ 𝑛 = 0 ) )
52 51 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( ¬ 𝑘 = 0 ↔ ¬ 𝑛 = 0 ) )
53 49 52 mpbird ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ¬ 𝑘 = 0 )
54 53 iffalsed ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → if ( 𝑘 = 0 , ( ( coe1 ‘ 𝑀 ) ‘ 0 ) , 0 ) = 0 )
55 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
56 55 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
57 2 fvexi ⊢ 0 ∈ V
58 57 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 0 ∈ V )
59 45 54 56 58 fvmptd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) = 0 )
60 59 eqcomd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 0 = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) )
61 60 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → 0 = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) )
62 42 61 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) )
63 62 ex ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 → ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ) )
64 63 ralimdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ) )
65 64 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) )
66 3 5 1 ply1sclid ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ∈ 𝐾 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) )
67 19 66 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) )
68 67 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) )
69 df-n0 ⊢ ℕ0 = ( ℕ ∪ { 0 } )
70 69 raleqi ⊢ ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( ℕ ∪ { 0 } ) ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) )
71 c0ex ⊢ 0 ∈ V
72 fveq2 ⊢ ( 𝑛 = 0 → ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ 𝑀 ) ‘ 0 ) )
73 fveq2 ⊢ ( 𝑛 = 0 → ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) )
74 72 73 eqeq12d ⊢ ( 𝑛 = 0 → ( ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ↔ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) ) )
75 74 ralunsn ⊢ ( 0 ∈ V → ( ∀ 𝑛 ∈ ( ℕ ∪ { 0 } ) ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ↔ ( ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) ) ) )
76 71 75 mp1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ( ∀ 𝑛 ∈ ( ℕ ∪ { 0 } ) ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ↔ ( ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) ) ) )
77 70 76 bitrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ↔ ( ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 0 ) ) ) )
78 65 68 77 mpbir2and ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) )
79 eqid ⊢ ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) = ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) )
80 3 4 17 79 eqcoe1ply1eq ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ∈ 𝐵 ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) ‘ 𝑛 ) → 𝑀 = ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) ) )
81 41 78 80 sylc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → 𝑀 = ( 𝐴 ‘ ( ( coe1 ‘ 𝑀 ) ‘ 0 ) ) )
82 20 23 81 rspcedvd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) → ∃ 𝑠 ∈ 𝐾 𝑀 = ( 𝐴 ‘ 𝑠 ) )
83 82 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 → ∃ 𝑠 ∈ 𝐾 𝑀 = ( 𝐴 ‘ 𝑠 ) ) )
84 14 83 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐾 𝑀 = ( 𝐴 ‘ 𝑠 ) ↔ ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ 𝑀 ) ‘ 𝑛 ) = 0 ) )