Metamath Proof Explorer


Theorem imasring

Description: The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses imasring.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasring.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasring.p + = ( +g𝑅 )
imasring.t · = ( .r𝑅 )
imasring.o 1 = ( 1r𝑅 )
imasring.f ( 𝜑𝐹 : 𝑉onto𝐵 )
imasring.e1 ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasring.e2 ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasring.r ( 𝜑𝑅 ∈ Ring )
Assertion imasring ( 𝜑 → ( 𝑈 ∈ Ring ∧ ( 𝐹1 ) = ( 1r𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 imasring.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
2 imasring.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
3 imasring.p + = ( +g𝑅 )
4 imasring.t · = ( .r𝑅 )
5 imasring.o 1 = ( 1r𝑅 )
6 imasring.f ( 𝜑𝐹 : 𝑉onto𝐵 )
7 imasring.e1 ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
8 imasring.e2 ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
9 imasring.r ( 𝜑𝑅 ∈ Ring )
10 1 2 6 9 imasbas ( 𝜑𝐵 = ( Base ‘ 𝑈 ) )
11 eqidd ( 𝜑 → ( +g𝑈 ) = ( +g𝑈 ) )
12 eqidd ( 𝜑 → ( .r𝑈 ) = ( .r𝑈 ) )
13 3 a1i ( 𝜑+ = ( +g𝑅 ) )
14 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
15 9 14 syl ( 𝜑𝑅 ∈ Grp )
16 eqid ( 0g𝑅 ) = ( 0g𝑅 )
17 1 2 13 6 7 15 16 imasgrp ( 𝜑 → ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ ( 0g𝑅 ) ) = ( 0g𝑈 ) ) )
18 17 simpld ( 𝜑𝑈 ∈ Grp )
19 eqid ( .r𝑈 ) = ( .r𝑈 )
20 9 adantr ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → 𝑅 ∈ Ring )
21 simprl ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → 𝑢𝑉 )
22 2 adantr ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
23 21 22 eleqtrd ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
24 simprr ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → 𝑣𝑉 )
25 24 22 eleqtrd ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → 𝑣 ∈ ( Base ‘ 𝑅 ) )
26 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 26 4 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 · 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
28 20 23 25 27 syl3anc ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → ( 𝑢 · 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
29 28 22 eleqtrrd ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → ( 𝑢 · 𝑣 ) ∈ 𝑉 )
30 29 caovclg ( ( 𝜑 ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
31 6 8 1 2 9 4 19 30 imasmulf ( 𝜑 → ( .r𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
32 fovrn ( ( ( .r𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵𝑢𝐵𝑣𝐵 ) → ( 𝑢 ( .r𝑈 ) 𝑣 ) ∈ 𝐵 )
33 31 32 syl3an1 ( ( 𝜑𝑢𝐵𝑣𝐵 ) → ( 𝑢 ( .r𝑈 ) 𝑣 ) ∈ 𝐵 )
34 forn ( 𝐹 : 𝑉onto𝐵 → ran 𝐹 = 𝐵 )
35 6 34 syl ( 𝜑 → ran 𝐹 = 𝐵 )
36 35 eleq2d ( 𝜑 → ( 𝑢 ∈ ran 𝐹𝑢𝐵 ) )
37 35 eleq2d ( 𝜑 → ( 𝑣 ∈ ran 𝐹𝑣𝐵 ) )
38 35 eleq2d ( 𝜑 → ( 𝑤 ∈ ran 𝐹𝑤𝐵 ) )
39 36 37 38 3anbi123d ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐹𝑤 ∈ ran 𝐹 ) ↔ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) )
40 fofn ( 𝐹 : 𝑉onto𝐵𝐹 Fn 𝑉 )
41 6 40 syl ( 𝜑𝐹 Fn 𝑉 )
42 fvelrnb ( 𝐹 Fn 𝑉 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ) )
43 fvelrnb ( 𝐹 Fn 𝑉 → ( 𝑣 ∈ ran 𝐹 ↔ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ) )
44 fvelrnb ( 𝐹 Fn 𝑉 → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) )
45 42 43 44 3anbi123d ( 𝐹 Fn 𝑉 → ( ( 𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐹𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) ) )
46 41 45 syl ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐹𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) ) )
47 39 46 bitr3d ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) ) )
48 3reeanv ( ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) )
49 47 48 bitr4di ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ↔ ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) ) )
50 9 adantr ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑅 ∈ Ring )
51 simp2 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑥𝑉 )
52 2 3ad2ant1 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑉 = ( Base ‘ 𝑅 ) )
53 51 52 eleqtrd ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
54 53 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
55 simp3 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑦𝑉 )
56 55 52 eleqtrd ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
57 56 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
58 simpr3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑧𝑉 )
59 2 adantr ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
60 58 59 eleqtrd ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
61 26 4 ringass ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
62 50 54 57 60 61 syl13anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
63 62 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
64 simpl ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝜑 )
65 29 caovclg ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑉 )
66 65 3adantr3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑉 )
67 6 8 1 2 9 4 19 imasmulval ( ( 𝜑 ∧ ( 𝑥 · 𝑦 ) ∈ 𝑉𝑧𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) )
68 64 66 58 67 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) )
69 simpr1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑥𝑉 )
70 29 caovclg ( ( 𝜑 ∧ ( 𝑦𝑉𝑧𝑉 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝑉 )
71 70 3adantr1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝑉 )
72 6 8 1 2 9 4 19 imasmulval ( ( 𝜑𝑥𝑉 ∧ ( 𝑦 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
73 64 69 71 72 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
74 63 68 73 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
75 6 8 1 2 9 4 19 imasmulval ( ( 𝜑𝑥𝑉𝑦𝑉 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) )
76 75 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) )
77 76 oveq1d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) )
78 6 8 1 2 9 4 19 imasmulval ( ( 𝜑𝑦𝑉𝑧𝑉 ) → ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) )
79 78 3adant3r1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) )
80 79 oveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
81 74 77 80 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) )
82 simp1 ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝐹𝑥 ) = 𝑢 )
83 simp2 ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝐹𝑦 ) = 𝑣 )
84 82 83 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) = ( 𝑢 ( .r𝑈 ) 𝑣 ) )
85 simp3 ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝐹𝑧 ) = 𝑤 )
86 84 85 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) )
87 83 85 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝑣 ( .r𝑈 ) 𝑤 ) )
88 82 87 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) )
89 86 88 eqeq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) ↔ ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
90 81 89 syl5ibcom ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
91 90 3exp2 ( 𝜑 → ( 𝑥𝑉 → ( 𝑦𝑉 → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) ) ) ) )
92 91 imp32 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) ) )
93 92 rexlimdv ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( ∃ 𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
94 93 rexlimdvva ( 𝜑 → ( ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
95 49 94 sylbid ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) → ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
96 95 imp ( ( 𝜑 ∧ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) → ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) )
97 26 3 4 ringdi ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
98 50 54 57 60 97 syl13anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
99 98 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
100 26 3 ringacl ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 + 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
101 20 23 25 100 syl3anc ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → ( 𝑢 + 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
102 101 22 eleqtrrd ( ( 𝜑 ∧ ( 𝑢𝑉𝑣𝑉 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝑉 )
103 102 caovclg ( ( 𝜑 ∧ ( 𝑦𝑉𝑧𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
104 103 3adantr1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
105 6 8 1 2 9 4 19 imasmulval ( ( 𝜑𝑥𝑉 ∧ ( 𝑦 + 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) )
106 64 69 104 105 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) )
107 29 caovclg ( ( 𝜑 ∧ ( 𝑥𝑉𝑧𝑉 ) ) → ( 𝑥 · 𝑧 ) ∈ 𝑉 )
108 107 3adantr2 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑥 · 𝑧 ) ∈ 𝑉 )
109 eqid ( +g𝑈 ) = ( +g𝑈 )
110 6 7 1 2 9 3 109 imasaddval ( ( 𝜑 ∧ ( 𝑥 · 𝑦 ) ∈ 𝑉 ∧ ( 𝑥 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
111 64 66 108 110 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
112 99 106 111 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) )
113 6 7 1 2 9 3 109 imasaddval ( ( 𝜑𝑦𝑉𝑧𝑉 ) → ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
114 113 3adant3r1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
115 114 oveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) )
116 6 8 1 2 9 4 19 imasmulval ( ( 𝜑𝑥𝑉𝑧𝑉 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) )
117 116 3adant3r2 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) )
118 76 117 oveq12d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) )
119 112 115 118 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) )
120 83 85 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝑣 ( +g𝑈 ) 𝑤 ) )
121 82 120 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) = ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) )
122 82 85 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝑢 ( .r𝑈 ) 𝑤 ) )
123 84 122 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) )
124 121 123 eqeq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) ↔ ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) ) )
125 119 124 syl5ibcom ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) ) )
126 125 3exp2 ( 𝜑 → ( 𝑥𝑉 → ( 𝑦𝑉 → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) ) ) ) ) )
127 126 imp32 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) ) ) )
128 127 rexlimdv ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( ∃ 𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) ) )
129 128 rexlimdvva ( 𝜑 → ( ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) ) )
130 49 129 sylbid ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) → ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) ) )
131 130 imp ( ( 𝜑 ∧ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) → ( 𝑢 ( .r𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑣 ) ( +g𝑈 ) ( 𝑢 ( .r𝑈 ) 𝑤 ) ) )
132 26 3 4 ringdir ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
133 50 54 57 60 132 syl13anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
134 133 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
135 102 caovclg ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
136 135 3adantr3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
137 6 8 1 2 9 4 19 imasmulval ( ( 𝜑 ∧ ( 𝑥 + 𝑦 ) ∈ 𝑉𝑧𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) )
138 64 136 58 137 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) )
139 6 7 1 2 9 3 109 imasaddval ( ( 𝜑 ∧ ( 𝑥 · 𝑧 ) ∈ 𝑉 ∧ ( 𝑦 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
140 64 108 71 139 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
141 134 138 140 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
142 6 7 1 2 9 3 109 imasaddval ( ( 𝜑𝑥𝑉𝑦𝑉 ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
143 142 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
144 143 oveq1d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) )
145 117 79 oveq12d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
146 141 144 145 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) )
147 82 83 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) = ( 𝑢 ( +g𝑈 ) 𝑣 ) )
148 147 85 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) )
149 122 87 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) )
150 148 149 eqeq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( .r𝑈 ) ( 𝐹𝑧 ) ) = ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( .r𝑈 ) ( 𝐹𝑧 ) ) ) ↔ ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
151 146 150 syl5ibcom ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
152 151 3exp2 ( 𝜑 → ( 𝑥𝑉 → ( 𝑦𝑉 → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) ) ) ) )
153 152 imp32 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) ) )
154 153 rexlimdv ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( ∃ 𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
155 154 rexlimdvva ( 𝜑 → ( ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
156 49 155 sylbid ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) ) )
157 156 imp ( ( 𝜑 ∧ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( .r𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r𝑈 ) 𝑤 ) ( +g𝑈 ) ( 𝑣 ( .r𝑈 ) 𝑤 ) ) )
158 fof ( 𝐹 : 𝑉onto𝐵𝐹 : 𝑉𝐵 )
159 6 158 syl ( 𝜑𝐹 : 𝑉𝐵 )
160 26 5 ringidcl ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
161 9 160 syl ( 𝜑1 ∈ ( Base ‘ 𝑅 ) )
162 161 2 eleqtrrd ( 𝜑1𝑉 )
163 159 162 ffvelrnd ( 𝜑 → ( 𝐹1 ) ∈ 𝐵 )
164 41 42 syl ( 𝜑 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ) )
165 36 164 bitr3d ( 𝜑 → ( 𝑢𝐵 ↔ ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ) )
166 simpl ( ( 𝜑𝑥𝑉 ) → 𝜑 )
167 162 adantr ( ( 𝜑𝑥𝑉 ) → 1𝑉 )
168 simpr ( ( 𝜑𝑥𝑉 ) → 𝑥𝑉 )
169 6 8 1 2 9 4 19 imasmulval ( ( 𝜑1𝑉𝑥𝑉 ) → ( ( 𝐹1 ) ( .r𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 1 · 𝑥 ) ) )
170 166 167 168 169 syl3anc ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹1 ) ( .r𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 1 · 𝑥 ) ) )
171 2 eleq2d ( 𝜑 → ( 𝑥𝑉𝑥 ∈ ( Base ‘ 𝑅 ) ) )
172 171 biimpa ( ( 𝜑𝑥𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
173 26 4 5 ringlidm ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 1 · 𝑥 ) = 𝑥 )
174 9 172 173 syl2an2r ( ( 𝜑𝑥𝑉 ) → ( 1 · 𝑥 ) = 𝑥 )
175 174 fveq2d ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 1 · 𝑥 ) ) = ( 𝐹𝑥 ) )
176 170 175 eqtrd ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹1 ) ( .r𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) )
177 oveq2 ( ( 𝐹𝑥 ) = 𝑢 → ( ( 𝐹1 ) ( .r𝑈 ) ( 𝐹𝑥 ) ) = ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) )
178 id ( ( 𝐹𝑥 ) = 𝑢 → ( 𝐹𝑥 ) = 𝑢 )
179 177 178 eqeq12d ( ( 𝐹𝑥 ) = 𝑢 → ( ( ( 𝐹1 ) ( .r𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) ↔ ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ) )
180 176 179 syl5ibcom ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑥 ) = 𝑢 → ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ) )
181 180 rexlimdva ( 𝜑 → ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 → ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ) )
182 165 181 sylbid ( 𝜑 → ( 𝑢𝐵 → ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ) )
183 182 imp ( ( 𝜑𝑢𝐵 ) → ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 )
184 6 8 1 2 9 4 19 imasmulval ( ( 𝜑𝑥𝑉1𝑉 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹1 ) ) = ( 𝐹 ‘ ( 𝑥 · 1 ) ) )
185 167 184 mpd3an3 ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹1 ) ) = ( 𝐹 ‘ ( 𝑥 · 1 ) ) )
186 26 4 5 ringridm ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 · 1 ) = 𝑥 )
187 9 172 186 syl2an2r ( ( 𝜑𝑥𝑉 ) → ( 𝑥 · 1 ) = 𝑥 )
188 187 fveq2d ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 𝑥 · 1 ) ) = ( 𝐹𝑥 ) )
189 185 188 eqtrd ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹1 ) ) = ( 𝐹𝑥 ) )
190 oveq1 ( ( 𝐹𝑥 ) = 𝑢 → ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹1 ) ) = ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) )
191 190 178 eqeq12d ( ( 𝐹𝑥 ) = 𝑢 → ( ( ( 𝐹𝑥 ) ( .r𝑈 ) ( 𝐹1 ) ) = ( 𝐹𝑥 ) ↔ ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) )
192 189 191 syl5ibcom ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑥 ) = 𝑢 → ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) )
193 192 rexlimdva ( 𝜑 → ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 → ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) )
194 165 193 sylbid ( 𝜑 → ( 𝑢𝐵 → ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) )
195 194 imp ( ( 𝜑𝑢𝐵 ) → ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 )
196 10 11 12 18 33 96 131 157 163 183 195 isringd ( 𝜑𝑈 ∈ Ring )
197 163 10 eleqtrd ( 𝜑 → ( 𝐹1 ) ∈ ( Base ‘ 𝑈 ) )
198 10 eleq2d ( 𝜑 → ( 𝑢𝐵𝑢 ∈ ( Base ‘ 𝑈 ) ) )
199 182 194 jcad ( 𝜑 → ( 𝑢𝐵 → ( ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) ) )
200 198 199 sylbird ( 𝜑 → ( 𝑢 ∈ ( Base ‘ 𝑈 ) → ( ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) ) )
201 200 ralrimiv ( 𝜑 → ∀ 𝑢 ∈ ( Base ‘ 𝑈 ) ( ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) )
202 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
203 eqid ( 1r𝑈 ) = ( 1r𝑈 )
204 202 19 203 isringid ( 𝑈 ∈ Ring → ( ( ( 𝐹1 ) ∈ ( Base ‘ 𝑈 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑈 ) ( ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) ) ↔ ( 1r𝑈 ) = ( 𝐹1 ) ) )
205 196 204 syl ( 𝜑 → ( ( ( 𝐹1 ) ∈ ( Base ‘ 𝑈 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑈 ) ( ( ( 𝐹1 ) ( .r𝑈 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r𝑈 ) ( 𝐹1 ) ) = 𝑢 ) ) ↔ ( 1r𝑈 ) = ( 𝐹1 ) ) )
206 197 201 205 mpbi2and ( 𝜑 → ( 1r𝑈 ) = ( 𝐹1 ) )
207 206 eqcomd ( 𝜑 → ( 𝐹1 ) = ( 1r𝑈 ) )
208 196 207 jca ( 𝜑 → ( 𝑈 ∈ Ring ∧ ( 𝐹1 ) = ( 1r𝑈 ) ) )