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	$⊢ φ \to U = F “_{𝑠} R$
	imasrng.v	$⊢ φ \to V = {Base}_{R}$
	imasrng.p	$⊢ \underset{˙}{+} = +_{R}$
	imasrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	imasrng.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasrng.e1	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
	imasrng.e2	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
	imasrng.r	$⊢ φ \to R \in Rng$
Assertion	imasrng	$⊢ φ \to U \in Rng$

Proof

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

Metamath Proof Explorer

Theorem imasrng

Proof