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

Metamath Proof Explorer

Theorem imasrng

Description: The image structure of a non-unital ring is a non-unital ring ( imasring analog). (Contributed by AV, 22-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 imasrng.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasrng.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasrng.p ⊢ + = ( +g ‘ 𝑅 )
4 imasrng.t ⊢ · = ( .r ‘ 𝑅 )
5 imasrng.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
6 imasrng.e1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
7 imasrng.e2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
8 imasrng.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
9 1 2 5 8 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
10 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 ) )
11 eqidd ⊢ ( 𝜑 → ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 ) )
12 3 a1i ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
13 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
14 8 13 syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
15 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16 1 2 12 5 6 14 15 imasabl ⊢ ( 𝜑 → ( 𝑈 ∈ Abel ∧ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑈 ) ) )
17 16 simpld ⊢ ( 𝜑 → 𝑈 ∈ Abel )
18 eqid ⊢ ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 )
19 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑅 ∈ Rng )
20 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑢 ∈ 𝑉 )
21 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
22 20 21 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
23 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑣 ∈ 𝑉 )
24 23 21 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑣 ∈ ( Base ‘ 𝑅 ) )
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 25 4 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 · 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
27 19 22 24 26 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝑢 · 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
28 27 21 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝑢 · 𝑣 ) ∈ 𝑉 )
29 28 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
30 5 7 1 2 8 4 18 29 imasmulf ⊢ ( 𝜑 → ( .r ‘ 𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
31 30 fovcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ∈ 𝐵 )
32 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
33 5 32 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
34 33 eleq2d ⊢ ( 𝜑 → ( 𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵 ) )
35 33 eleq2d ⊢ ( 𝜑 → ( 𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵 ) )
36 33 eleq2d ⊢ ( 𝜑 → ( 𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵 ) )
37 34 35 36 3anbi123d ⊢ ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹 ) ↔ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) )
38 fofn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 Fn 𝑉 )
39 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
40 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑣 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ) )
41 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) )
42 39 40 41 3anbi123d ⊢ ( 𝐹 Fn 𝑉 → ( ( 𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
43 5 38 42 3syl ⊢ ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
44 37 43 bitr3d ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
45 3reeanv ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) )
46 44 45 bitr4di ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
47 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑅 ∈ Rng )
48 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
49 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑉 = ( Base ‘ 𝑅 ) )
50 48 49 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
51 50 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
52 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝑉 )
53 52 49 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
54 53 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
55 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ 𝑉 )
56 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
57 55 56 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
58 25 4 rngass ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
59 47 51 54 57 58 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
60 59 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
61 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝜑 )
62 28 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑉 )
63 62 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑉 )
64 5 7 1 2 8 4 18 imasmulval ⊢ ( ( 𝜑 ∧ ( 𝑥 · 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) )
65 61 63 55 64 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) )
66 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 )
67 28 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝑉 )
68 67 3adantr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝑉 )
69 5 7 1 2 8 4 18 imasmulval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝑦 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
70 61 66 68 69 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
71 60 65 70 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
72 5 7 1 2 8 4 18 imasmulval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) )
73 72 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) )
74 73 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) )
75 5 7 1 2 8 4 18 imasmulval ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) )
76 75 3adant3r1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) )
77 76 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
78 71 74 77 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) )
79 simp1 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑥 ) = 𝑢 )
80 simp2 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑦 ) = 𝑣 )
81 79 80 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) )
82 simp3 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = 𝑤 )
83 81 82 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) )
84 80 82 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) )
85 79 84 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) )
86 83 85 eqeq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
87 78 86 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
88 87 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑉 → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) ) ) ) )
89 88 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) ) )
90 89 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
91 90 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
92 46 91 sylbid ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
93 92 imp ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) )
94 25 3 4 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
95 47 51 54 57 94 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
96 95 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
97 25 3 rngacl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 + 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
98 19 22 24 97 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝑢 + 𝑣 ) ∈ ( Base ‘ 𝑅 ) )
99 98 21 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝑉 )
100 99 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
101 100 3adantr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
102 5 7 1 2 8 4 18 imasmulval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝑦 + 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) )
103 61 66 101 102 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) )
104 28 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 · 𝑧 ) ∈ 𝑉 )
105 104 3adantr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 · 𝑧 ) ∈ 𝑉 )
106 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
107 5 6 1 2 8 3 106 imasaddval ⊢ ( ( 𝜑 ∧ ( 𝑥 · 𝑦 ) ∈ 𝑉 ∧ ( 𝑥 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
108 61 63 105 107 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
109 96 103 108 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) )
110 5 6 1 2 8 3 106 imasaddval ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
111 110 3adant3r1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
112 111 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) )
113 5 7 1 2 8 4 18 imasmulval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) )
114 113 3adant3r2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) )
115 73 114 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ) )
116 109 112 115 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) )
117 80 82 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) )
118 79 117 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) )
119 79 82 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) )
120 81 119 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) )
121 118 120 eqeq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
122 116 121 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
123 122 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑉 → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) ) ) ) ) )
124 123 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) ) ) )
125 124 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
126 125 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
127 46 126 sylbid ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
128 127 imp ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑢 ( .r ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ) )
129 25 3 4 rngdir ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
130 47 51 54 57 129 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
131 130 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
132 99 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
133 132 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
134 5 7 1 2 8 4 18 imasmulval ⊢ ( ( 𝜑 ∧ ( 𝑥 + 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) )
135 61 133 55 134 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) )
136 5 6 1 2 8 3 106 imasaddval ⊢ ( ( 𝜑 ∧ ( 𝑥 · 𝑧 ) ∈ 𝑉 ∧ ( 𝑦 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
137 61 105 68 136 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
138 131 135 137 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
139 5 6 1 2 8 3 106 imasaddval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
140 139 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
141 140 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) )
142 114 76 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ ( 𝑥 · 𝑧 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) ) )
143 138 141 142 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) )
144 79 80 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) )
145 144 82 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) )
146 119 84 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) )
147 145 146 eqeq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
148 143 147 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
149 148 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑉 → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) ) ) ) )
150 149 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) ) )
151 150 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
152 151 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
153 46 152 sylbid ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) ) )
154 153 imp ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( .r ‘ 𝑈 ) 𝑤 ) = ( ( 𝑢 ( .r ‘ 𝑈 ) 𝑤 ) ( +g ‘ 𝑈 ) ( 𝑣 ( .r ‘ 𝑈 ) 𝑤 ) ) )
155 9 10 11 17 31 93 128 154 isrngd ⊢ ( 𝜑 → 𝑈 ∈ Rng )