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

Metamath Proof Explorer

Theorem ply1dg1rt

Description: Express the root - B / A of a polynomial A x. X + B of degree 1 over a field. (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Hypotheses ply1dg1rt.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1dg1rt.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
ply1dg1rt.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
ply1dg1rt.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ply1dg1rt.0 ⊢ 0 = ( 0g ‘ 𝑅 )
ply1dg1rt.r ⊢ ( 𝜑 → 𝑅 ∈ Field )
ply1dg1rt.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
ply1dg1rt.1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 1 )
ply1dg1rt.x ⊢ 𝑁 = ( invg ‘ 𝑅 )
ply1dg1rt.m ⊢ / = ( /r ‘ 𝑅 )
ply1dg1rt.c ⊢ 𝐶 = ( coe1 ‘ 𝐺 )
ply1dg1rt.a ⊢ 𝐴 = ( 𝐶 ‘ 1 )
ply1dg1rt.b ⊢ 𝐵 = ( 𝐶 ‘ 0 )
ply1dg1rt.z ⊢ 𝑍 = ( ( 𝑁 ‘ 𝐵 ) / 𝐴 )
Assertion ply1dg1rt ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑍 } )

Proof

Step Hyp Ref Expression
1 ply1dg1rt.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1dg1rt.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 ply1dg1rt.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
4 ply1dg1rt.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5 ply1dg1rt.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 ply1dg1rt.r ⊢ ( 𝜑 → 𝑅 ∈ Field )
7 ply1dg1rt.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
8 ply1dg1rt.1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 1 )
9 ply1dg1rt.x ⊢ 𝑁 = ( invg ‘ 𝑅 )
10 ply1dg1rt.m ⊢ / = ( /r ‘ 𝑅 )
11 ply1dg1rt.c ⊢ 𝐶 = ( coe1 ‘ 𝐺 )
12 ply1dg1rt.a ⊢ 𝐴 = ( 𝐶 ‘ 1 )
13 ply1dg1rt.b ⊢ 𝐵 = ( 𝐶 ‘ 0 )
14 ply1dg1rt.z ⊢ 𝑍 = ( ( 𝑁 ‘ 𝐵 ) / 𝐴 )
15 6 fldcrngd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
16 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17 3 1 2 15 16 7 evl1fvf ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
18 17 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) Fn ( Base ‘ 𝑅 ) )
19 fniniseg2 ⊢ ( ( 𝑂 ‘ 𝐺 ) Fn ( Base ‘ 𝑅 ) → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 } )
20 18 19 syl ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 } )
21 fveqeq2 ⊢ ( 𝑥 = 𝑍 → ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 ) )
22 15 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
23 15 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
24 0nn0 ⊢ 0 ∈ ℕ0
25 11 2 1 16 coe1fvalcl ⊢ ( ( 𝐺 ∈ 𝑈 ∧ 0 ∈ ℕ0 ) → ( 𝐶 ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
26 7 24 25 sylancl ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
27 13 26 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ 𝑅 ) )
28 16 9 23 27 grpinvcld ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐵 ) ∈ ( Base ‘ 𝑅 ) )
29 6 flddrngd ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
30 1nn0 ⊢ 1 ∈ ℕ0
31 11 2 1 16 coe1fvalcl ⊢ ( ( 𝐺 ∈ 𝑈 ∧ 1 ∈ ℕ0 ) → ( 𝐶 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) )
32 7 30 31 sylancl ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) )
33 8 fveq2d ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 𝐶 ‘ 1 ) )
34 8 30 eqeltrdi ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
35 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
36 4 1 35 2 deg1nn0clb ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝑈 ) → ( 𝐺 ≠ ( 0g ‘ 𝑃 ) ↔ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) )
37 36 biimpar ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝑈 ) ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
38 22 7 34 37 syl21anc ⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
39 4 1 35 2 5 11 deg1ldg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝑈 ∧ 𝐺 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐶 ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ 0 )
40 22 7 38 39 syl3anc ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ 0 )
41 33 40 eqnetrrd ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) ≠ 0 )
42 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
43 16 42 5 drngunit ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐶 ‘ 1 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐶 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐶 ‘ 1 ) ≠ 0 ) ) )
44 43 biimpar ⊢ ( ( 𝑅 ∈ DivRing ∧ ( ( 𝐶 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐶 ‘ 1 ) ≠ 0 ) ) → ( 𝐶 ‘ 1 ) ∈ ( Unit ‘ 𝑅 ) )
45 29 32 41 44 syl12anc ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) ∈ ( Unit ‘ 𝑅 ) )
46 12 45 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ ( Unit ‘ 𝑅 ) )
47 16 42 10 dvrcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝐵 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
48 22 28 46 47 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
49 14 48 eqeltrid ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝑅 ) )
50 eqidd ⊢ ( 𝜑 → 𝑍 = 𝑍 )
51 eqeq1 ⊢ ( 𝑥 = 𝑍 → ( 𝑥 = 𝑍 ↔ 𝑍 = 𝑍 ) )
52 51 imbi1d ⊢ ( 𝑥 = 𝑍 → ( ( 𝑥 = 𝑍 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 ) ↔ ( 𝑍 = 𝑍 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 ) ) )
53 fveq2 ⊢ ( 𝑥 = 𝑍 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) )
54 53 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 = 𝑍 ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) )
55 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
56 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
57 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
58 12 32 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑅 ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
60 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
61 16 56 57 59 60 ringcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
62 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝐵 ) ∈ ( Base ‘ 𝑅 ) )
63 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐵 ∈ ( Base ‘ 𝑅 ) )
64 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
65 16 64 grprcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑁 ‘ 𝐵 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝐵 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) = ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑅 ) 𝐵 ) ↔ ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑁 ‘ 𝐵 ) ) )
66 55 61 62 63 65 syl13anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) = ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑅 ) 𝐵 ) ↔ ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑁 ‘ 𝐵 ) ) )
67 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
68 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
69 16 56 67 68 59 crngcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ) )
70 46 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐴 ∈ ( Unit ‘ 𝑅 ) )
71 16 42 10 56 dvrcan1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝐵 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 𝑁 ‘ 𝐵 ) )
72 57 62 70 71 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 𝑁 ‘ 𝐵 ) )
73 69 72 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ) = ( 𝑁 ‘ 𝐵 ) )
74 73 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ) ↔ ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑁 ‘ 𝐵 ) ) )
75 drngdomn ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )
76 29 75 syl ⊢ ( 𝜑 → 𝑅 ∈ Domn )
77 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
78 76 77 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )
80 42 5 79 70 unitnz ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐴 ≠ 0 )
81 59 80 eldifsnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐴 ∈ ( ( Base ‘ 𝑅 ) ∖ { 0 } ) )
82 76 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Domn )
83 16 5 56 81 60 68 82 domnlcanb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ) ↔ 𝑥 = ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ) )
84 66 74 83 3bitr2rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 = ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ↔ ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) = ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑅 ) 𝐵 ) ) )
85 16 64 5 9 55 63 grplinvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑅 ) 𝐵 ) = 0 )
86 85 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) = ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑅 ) 𝐵 ) ↔ ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) = 0 ) )
87 84 86 bitr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) = 0 ↔ 𝑥 = ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ) )
88 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐺 ∈ 𝑈 )
89 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝐺 ) = 1 )
90 1 3 16 2 56 64 11 4 12 13 67 88 89 60 evl1deg1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) )
91 90 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝐴 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝐵 ) = 0 ) )
92 14 eqeq2i ⊢ ( 𝑥 = 𝑍 ↔ 𝑥 = ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) )
93 92 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 = 𝑍 ↔ 𝑥 = ( ( 𝑁 ‘ 𝐵 ) / 𝐴 ) ) )
94 87 91 93 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = 𝑍 ) )
95 94 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 = 𝑍 ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 )
96 54 95 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 = 𝑍 ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 )
97 96 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 = 𝑍 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 ) )
98 97 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 = 𝑍 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 ) )
99 52 98 49 rspcdva ⊢ ( 𝜑 → ( 𝑍 = 𝑍 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 ) )
100 50 99 mpd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑍 ) = 0 )
101 94 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ) → 𝑥 = 𝑍 )
102 21 49 100 101 rabeqsnd ⊢ ( 𝜑 → { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 } = { 𝑍 } )
103 20 102 eqtrd ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑍 } )