Metamath Proof Explorer

Theorem deg1mhm

Description: Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses deg1mhm.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1mhm.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
deg1mhm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
deg1mhm.z ⊢ 0 = ( 0g ‘ 𝑃 )
deg1mhm.y ⊢ 𝑌 = ( ( mulGrp ‘ 𝑃 ) ↾s ( 𝐵 ∖ { 0 } ) )
deg1mhm.n ⊢ 𝑁 = ( ℂfld ↾s ℕ0 )
Assertion deg1mhm ( 𝑅 ∈ Domn → ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ∈ ( 𝑌 MndHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 deg1mhm.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1mhm.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 deg1mhm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 deg1mhm.z ⊢ 0 = ( 0g ‘ 𝑃 )
5 deg1mhm.y ⊢ 𝑌 = ( ( mulGrp ‘ 𝑃 ) ↾s ( 𝐵 ∖ { 0 } ) )
6 deg1mhm.n ⊢ 𝑁 = ( ℂfld ↾s ℕ0 )
7 3 ply1domn ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )
8 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
9 2 4 8 isdomn3 ⊢ ( 𝑃 ∈ Domn ↔ ( 𝑃 ∈ Ring ∧ ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑃 ) ) ) )
10 9 simprbi ⊢ ( 𝑃 ∈ Domn → ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑃 ) ) )
11 7 10 syl ⊢ ( 𝑅 ∈ Domn → ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑃 ) ) )
12 5 submmnd ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑃 ) ) → 𝑌 ∈ Mnd )
13 11 12 syl ⊢ ( 𝑅 ∈ Domn → 𝑌 ∈ Mnd )
14 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
15 6 submmnd ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 𝑁 ∈ Mnd )
16 14 15 mp1i ⊢ ( 𝑅 ∈ Domn → 𝑁 ∈ Mnd )
17 13 16 jca ⊢ ( 𝑅 ∈ Domn → ( 𝑌 ∈ Mnd ∧ 𝑁 ∈ Mnd ) )
18 1 3 2 deg1xrf ⊢ 𝐷 : 𝐵 ⟶ ℝ*
19 ffn ⊢ ( 𝐷 : 𝐵 ⟶ ℝ* → 𝐷 Fn 𝐵 )
20 18 19 ax-mp ⊢ 𝐷 Fn 𝐵
21 difss ⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
22 fnssres ⊢ ( ( 𝐷 Fn 𝐵 ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ) → ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) Fn ( 𝐵 ∖ { 0 } ) )
23 20 21 22 mp2an ⊢ ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) Fn ( 𝐵 ∖ { 0 } )
24 23 a1i ⊢ ( 𝑅 ∈ Domn → ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) Fn ( 𝐵 ∖ { 0 } ) )
25 fvres ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝑥 ) )
26 25 adantl ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝑥 ) )
27 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
28 27 adantr ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
29 eldifi ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ∈ 𝐵 )
30 29 adantl ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ 𝐵 )
31 eldifsni ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ≠ 0 )
32 31 adantl ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ≠ 0 )
33 1 3 4 2 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → ( 𝐷 ‘ 𝑥 ) ∈ ℕ0 )
34 28 30 32 33 syl3anc ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝐷 ‘ 𝑥 ) ∈ ℕ0 )
35 26 34 eqeltrd ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) ∈ ℕ0 )
36 35 ralrimiva ⊢ ( 𝑅 ∈ Domn → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) ∈ ℕ0 )
37 ffnfv ⊢ ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ↔ ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) Fn ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) ∈ ℕ0 ) )
38 24 36 37 sylanbrc ⊢ ( 𝑅 ∈ Domn → ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 )
39 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
40 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
41 27 adantr ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑅 ∈ Ring )
42 29 ad2antrl ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑥 ∈ 𝐵 )
43 31 ad2antrl ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑥 ≠ 0 )
44 simpl ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑅 ∈ Domn )
45 eqid ⊢ ( coe1 ‘ 𝑥 ) = ( coe1 ‘ 𝑥 )
46 1 3 4 2 39 45 deg1ldgdomn ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → ( ( coe1 ‘ 𝑥 ) ‘ ( 𝐷 ‘ 𝑥 ) ) ∈ ( RLReg ‘ 𝑅 ) )
47 44 42 43 46 syl3anc ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( coe1 ‘ 𝑥 ) ‘ ( 𝐷 ‘ 𝑥 ) ) ∈ ( RLReg ‘ 𝑅 ) )
48 eldifi ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → 𝑦 ∈ 𝐵 )
49 48 ad2antll ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑦 ∈ 𝐵 )
50 eldifsni ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → 𝑦 ≠ 0 )
51 50 ad2antll ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑦 ≠ 0 )
52 1 3 39 2 40 4 41 42 43 47 49 51 deg1mul2 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝐷 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐷 ‘ 𝑥 ) + ( 𝐷 ‘ 𝑦 ) ) )
53 domnring ⊢ ( 𝑃 ∈ Domn → 𝑃 ∈ Ring )
54 7 53 syl ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Ring )
55 54 adantr ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑃 ∈ Ring )
56 2 40 ringcl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
57 55 42 49 56 syl3anc ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
58 7 adantr ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑃 ∈ Domn )
59 2 40 4 domnmuln0 ⊢ ( ( 𝑃 ∈ Domn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ 0 )
60 58 42 43 49 51 59 syl122anc ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ 0 )
61 eldifsn ⊢ ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 ∧ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ 0 ) )
62 57 60 61 sylanbrc ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
63 fvres ⊢ ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( 𝐷 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
64 62 63 syl ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( 𝐷 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
65 fvres ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) = ( 𝐷 ‘ 𝑦 ) )
66 25 65 oveqan12d ⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) + ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) = ( ( 𝐷 ‘ 𝑥 ) + ( 𝐷 ‘ 𝑦 ) ) )
67 66 adantl ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) + ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) = ( ( 𝐷 ‘ 𝑥 ) + ( 𝐷 ‘ 𝑦 ) ) )
68 52 64 67 3eqtr4d ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) + ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) )
69 68 ralrimivva ⊢ ( 𝑅 ∈ Domn → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) + ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) )
70 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
71 2 70 ringidcl ⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
72 54 71 syl ⊢ ( 𝑅 ∈ Domn → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
73 domnnzr ⊢ ( 𝑃 ∈ Domn → 𝑃 ∈ NzRing )
74 70 4 nzrnz ⊢ ( 𝑃 ∈ NzRing → ( 1r ‘ 𝑃 ) ≠ 0 )
75 7 73 74 3syl ⊢ ( 𝑅 ∈ Domn → ( 1r ‘ 𝑃 ) ≠ 0 )
76 eldifsn ⊢ ( ( 1r ‘ 𝑃 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 1r ‘ 𝑃 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑃 ) ≠ 0 ) )
77 72 75 76 sylanbrc ⊢ ( 𝑅 ∈ Domn → ( 1r ‘ 𝑃 ) ∈ ( 𝐵 ∖ { 0 } ) )
78 fvres ⊢ ( ( 1r ‘ 𝑃 ) ∈ ( 𝐵 ∖ { 0 } ) → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 1r ‘ 𝑃 ) ) = ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) )
79 77 78 syl ⊢ ( 𝑅 ∈ Domn → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 1r ‘ 𝑃 ) ) = ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) )
80 8 70 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) )
81 5 80 subm0 ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑃 ) ) → ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑌 ) )
82 11 81 syl ⊢ ( 𝑅 ∈ Domn → ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑌 ) )
83 82 fveq2d ⊢ ( 𝑅 ∈ Domn → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 1r ‘ 𝑃 ) ) = ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 0g ‘ 𝑌 ) ) )
84 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
85 eqid ⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
86 3 70 85 1 mon1pid ⊢ ( 𝑅 ∈ NzRing → ( ( 1r ‘ 𝑃 ) ∈ ( Monic1p ‘ 𝑅 ) ∧ ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) = 0 ) )
87 86 simprd ⊢ ( 𝑅 ∈ NzRing → ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) = 0 )
88 84 87 syl ⊢ ( 𝑅 ∈ Domn → ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) = 0 )
89 79 83 88 3eqtr3d ⊢ ( 𝑅 ∈ Domn → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 0g ‘ 𝑌 ) ) = 0 )
90 38 69 89 3jca ⊢ ( 𝑅 ∈ Domn → ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) + ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ∧ ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 0g ‘ 𝑌 ) ) = 0 ) )
91 8 2 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
92 5 91 ressbas2 ⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ 𝑌 ) )
93 21 92 ax-mp ⊢ ( 𝐵 ∖ { 0 } ) = ( Base ‘ 𝑌 )
94 nn0sscn ⊢ ℕ0 ⊆ ℂ
95 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
96 6 95 ressbas2 ⊢ ( ℕ0 ⊆ ℂ → ℕ0 = ( Base ‘ 𝑁 ) )
97 94 96 ax-mp ⊢ ℕ0 = ( Base ‘ 𝑁 )
98 2 fvexi ⊢ 𝐵 ∈ V
99 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V )
100 98 99 ax-mp ⊢ ( 𝐵 ∖ { 0 } ) ∈ V
101 8 40 mgpplusg ⊢ ( .r ‘ 𝑃 ) = ( +g ‘ ( mulGrp ‘ 𝑃 ) )
102 5 101 ressplusg ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → ( .r ‘ 𝑃 ) = ( +g ‘ 𝑌 ) )
103 100 102 ax-mp ⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝑌 )
104 nn0ex ⊢ ℕ0 ∈ V
105 cnfldadd ⊢ + = ( +g ‘ ℂfld )
106 6 105 ressplusg ⊢ ( ℕ0 ∈ V → + = ( +g ‘ 𝑁 ) )
107 104 106 ax-mp ⊢ + = ( +g ‘ 𝑁 )
108 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
109 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
110 6 109 subm0 ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 0 = ( 0g ‘ 𝑁 ) )
111 14 110 ax-mp ⊢ 0 = ( 0g ‘ 𝑁 )
112 93 97 103 107 108 111 ismhm ⊢ ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ∈ ( 𝑌 MndHom 𝑁 ) ↔ ( ( 𝑌 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) + ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ∧ ( ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ ( 0g ‘ 𝑌 ) ) = 0 ) ) )
113 17 90 112 sylanbrc ⊢ ( 𝑅 ∈ Domn → ( 𝐷 ↾ ( 𝐵 ∖ { 0 } ) ) ∈ ( 𝑌 MndHom 𝑁 ) )