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

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 fovcdm ⊢ ( ( ( .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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 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 ‘ 𝑈 ) ) )