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 )