imasring

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

	Ref	Expression
Hypotheses	imasring.u	$⊢ φ \to U = F “_{𝑠} R$
	imasring.v	$⊢ φ \to V = {Base}_{R}$
	imasring.p	$⊢ \underset{˙}{+} = +_{R}$
	imasring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	imasring.o	$⊢ \underset{˙}{1} = 1_{R}$
	imasring.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasring.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))$
	imasring.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))$
	imasring.r	$⊢ φ \to R \in Ring$
Assertion	imasring	$⊢ φ \to (U \in Ring \land F (\underset{˙}{1}) = 1_{U})$

Proof

Step	Hyp	Ref	Expression
1		imasring.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasring.v	$⊢ φ \to V = {Base}_{R}$
3		imasring.p	$⊢ \underset{˙}{+} = +_{R}$
4		imasring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		imasring.o	$⊢ \underset{˙}{1} = 1_{R}$
6		imasring.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
7		imasring.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))$
8		imasring.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))$
9		imasring.r	$⊢ φ \to R \in Ring$
10	1 2 6 9	imasbas	$⊢ φ \to B = {Base}_{U}$
11		eqidd	$⊢ φ \to +_{U} = +_{U}$
12		eqidd	$⊢ φ \to \cdot_{U} = \cdot_{U}$
13	3	a1i	$⊢ φ \to \underset{˙}{+} = +_{R}$
14		ringgrp	$⊢ R \in Ring \to R \in Grp$
15	9 14	syl	$⊢ φ \to R \in Grp$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	1 2 13 6 7 15 16	imasgrp	$⊢ φ \to (U \in Grp \land F (0_{R}) = 0_{U})$
18	17	simpld	$⊢ φ \to U \in Grp$
19		eqid	$⊢ \cdot_{U} = \cdot_{U}$
20	9	adantr	$⊢ (φ \land (u \in V \land v \in V)) \to R \in Ring$
21		simprl	$⊢ (φ \land (u \in V \land v \in V)) \to u \in V$
22	2	adantr	$⊢ (φ \land (u \in V \land v \in V)) \to V = {Base}_{R}$
23	21 22	eleqtrd	$⊢ (φ \land (u \in V \land v \in V)) \to u \in {Base}_{R}$
24		simprr	$⊢ (φ \land (u \in V \land v \in V)) \to v \in V$
25	24 22	eleqtrd	$⊢ (φ \land (u \in V \land v \in V)) \to v \in {Base}_{R}$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27	26 4	ringcl	$⊢ (R \in Ring \land u \in {Base}_{R} \land v \in {Base}_{R}) \to u \underset{˙}{\cdot} v \in {Base}_{R}$
28	20 23 25 27	syl3anc	$⊢ (φ \land (u \in V \land v \in V)) \to u \underset{˙}{\cdot} v \in {Base}_{R}$
29	28 22	eleqtrrd	$⊢ (φ \land (u \in V \land v \in V)) \to u \underset{˙}{\cdot} v \in V$
30	29	caovclg	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{\cdot} q \in V$
31	6 8 1 2 9 4 19 30	imasmulf	$⊢ φ \to \cdot_{U} : B \times B ⟶ B$
32		fovrn	$⊢ (\cdot_{U} : B \times B ⟶ B \land u \in B \land v \in B) \to u \cdot_{U} v \in B$
33	31 32	syl3an1	$⊢ (φ \land u \in B \land v \in B) \to u \cdot_{U} v \in B$
34		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
35	6 34	syl	$⊢ φ \to ran F = B$
36	35	eleq2d	$⊢ φ \to (u \in ran F \leftrightarrow u \in B)$
37	35	eleq2d	$⊢ φ \to (v \in ran F \leftrightarrow v \in B)$
38	35	eleq2d	$⊢ φ \to (w \in ran F \leftrightarrow w \in B)$
39	36 37 38	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))$
40		fofn	$⊢ F : V \underset{onto}{⟶} B \to F Fn V$
41	6 40	syl	$⊢ φ \to F Fn V$
42		fvelrnb	$⊢ F Fn V \to (u \in ran F \leftrightarrow \exists x \in V F (x) = u)$
43		fvelrnb	$⊢ F Fn V \to (v \in ran F \leftrightarrow \exists y \in V F (y) = v)$
44		fvelrnb	$⊢ F Fn V \to (w \in ran F \leftrightarrow \exists z \in V F (z) = w)$
45	42 43 44	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))$
46	41 45	syl	$⊢ φ \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))$
47	39 46	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))$
48		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)$
49	47 48	syl6bbr	$⊢ φ \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))$
50	9	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to R \in Ring$
51		simp2	$⊢ (φ \land x \in V \land y \in V) \to x \in V$
52	2	3ad2ant1	$⊢ (φ \land x \in V \land y \in V) \to V = {Base}_{R}$
53	51 52	eleqtrd	$⊢ (φ \land x \in V \land y \in V) \to x \in {Base}_{R}$
54	53	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \in {Base}_{R}$
55		simp3	$⊢ (φ \land x \in V \land y \in V) \to y \in V$
56	55 52	eleqtrd	$⊢ (φ \land x \in V \land y \in V) \to y \in {Base}_{R}$
57	56	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \in {Base}_{R}$
58		simpr3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in V$
59	2	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to V = {Base}_{R}$
60	58 59	eleqtrd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in {Base}_{R}$
61	26 4	ringass	$⊢ (R \in Ring \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)$
62	50 54 57 60 61	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)$
63	62	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))$
64		simpl	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to φ$
65	29	caovclg	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{\cdot} y \in V$
66	65	3adantr3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{\cdot} y \in V$
67	6 8 1 2 9 4 19	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)$
68	64 66 58 67	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)$
69		simpr1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \in V$
70	29	caovclg	$⊢ (φ \land (y \in V \land z \in V)) \to y \underset{˙}{\cdot} z \in V$
71	70	3adantr1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \underset{˙}{\cdot} z \in V$
72	6 8 1 2 9 4 19	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))$
73	64 69 71 72	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))$
74	63 68 73	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)$
75	6 8 1 2 9 4 19	imasmulval	$⊢ (φ \land x \in V \land y \in V) \to F (x) \cdot_{U} F (y) = F (x \underset{˙}{\cdot} y)$
76	75	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)$
77	76	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)$
78	6 8 1 2 9 4 19	imasmulval	$⊢ (φ \land y \in V \land z \in V) \to F (y) \cdot_{U} F (z) = F (y \underset{˙}{\cdot} z)$
79	78	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)$
80	79	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)$
81	74 77 80	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))$
82		simp1	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) = u$
83		simp2	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (y) = v$
84	82 83	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) \cdot_{U} F (y) = u \cdot_{U} v$
85		simp3	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (z) = w$
86	84 85	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$
87	83 85	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (y) \cdot_{U} F (z) = v \cdot_{U} w$
88	82 87	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)$
89	86 88	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))$
90	81 89	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))$
91	90	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)))))$
92	91	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)))$
93	92	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))$
94	93	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))$
95	49 94	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))$
96	95	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)$
97	26 3 4	ringdi	$⊢ (R \in Ring \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)$
98	50 54 57 60 97	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)$
99	98	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))$
100	26 3	ringacl	$⊢ (R \in Ring \land u \in {Base}_{R} \land v \in {Base}_{R}) \to u \underset{˙}{+} v \in {Base}_{R}$
101	20 23 25 100	syl3anc	$⊢ (φ \land (u \in V \land v \in V)) \to u \underset{˙}{+} v \in {Base}_{R}$
102	101 22	eleqtrrd	$⊢ (φ \land (u \in V \land v \in V)) \to u \underset{˙}{+} v \in V$
103	102	caovclg	$⊢ (φ \land (y \in V \land z \in V)) \to y \underset{˙}{+} z \in V$
104	103	3adantr1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \underset{˙}{+} z \in V$
105	6 8 1 2 9 4 19	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))$
106	64 69 104 105	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))$
107	29	caovclg	$⊢ (φ \land (x \in V \land z \in V)) \to x \underset{˙}{\cdot} z \in V$
108	107	3adantr2	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{\cdot} z \in V$
109		eqid	$⊢ +_{U} = +_{U}$
110	6 7 1 2 9 3 109	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))$
111	64 66 108 110	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))$
112	99 106 111	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)$
113	6 7 1 2 9 3 109	imasaddval	$⊢ (φ \land y \in V \land z \in V) \to F (y) +_{U} F (z) = F (y \underset{˙}{+} z)$
114	113	3adant3r1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (y) +_{U} F (z) = F (y \underset{˙}{+} z)$
115	114	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)$
116	6 8 1 2 9 4 19	imasmulval	$⊢ (φ \land x \in V \land z \in V) \to F (x) \cdot_{U} F (z) = F (x \underset{˙}{\cdot} z)$
117	116	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)$
118	76 117	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)$
119	112 115 118	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))$
120	83 85	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (y) +_{U} F (z) = v +_{U} w$
121	82 120	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)$
122	82 85	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) \cdot_{U} F (z) = u \cdot_{U} w$
123	84 122	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)$
124	121 123	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))$
125	119 124	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))$
126	125	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)))))$
127	126	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)))$
128	127	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))$
129	128	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))$
130	49 129	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))$
131	130	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)$
132	26 3 4	ringdir	$⊢ (R \in Ring \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)$
133	50 54 57 60 132	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)$
134	133	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))$
135	102	caovclg	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in V$
136	135	3adantr3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{+} y \in V$
137	6 8 1 2 9 4 19	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)$
138	64 136 58 137	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)$
139	6 7 1 2 9 3 109	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))$
140	64 108 71 139	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))$
141	134 138 140	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)$
142	6 7 1 2 9 3 109	imasaddval	$⊢ (φ \land x \in V \land y \in V) \to F (x) +_{U} F (y) = F (x \underset{˙}{+} y)$
143	142	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x) +_{U} F (y) = F (x \underset{˙}{+} y)$
144	143	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)$
145	117 79	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)$
146	141 144 145	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))$
147	82 83	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) +_{U} F (y) = u +_{U} v$
148	147 85	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$
149	122 87	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)$
150	148 149	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))$
151	146 150	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))$
152	151	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)))))$
153	152	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)))$
154	153	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))$
155	154	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))$
156	49 155	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))$
157	156	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)$
158		fof	$⊢ F : V \underset{onto}{⟶} B \to F : V ⟶ B$
159	6 158	syl	$⊢ φ \to F : V ⟶ B$
160	26 5	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
161	9 160	syl	$⊢ φ \to \underset{˙}{1} \in {Base}_{R}$
162	161 2	eleqtrrd	$⊢ φ \to \underset{˙}{1} \in V$
163	159 162	ffvelrnd	$⊢ φ \to F (\underset{˙}{1}) \in B$
164	41 42	syl	$⊢ φ \to (u \in ran F \leftrightarrow \exists x \in V F (x) = u)$
165	36 164	bitr3d	$⊢ φ \to (u \in B \leftrightarrow \exists x \in V F (x) = u)$
166		simpl	$⊢ (φ \land x \in V) \to φ$
167	162	adantr	$⊢ (φ \land x \in V) \to \underset{˙}{1} \in V$
168		simpr	$⊢ (φ \land x \in V) \to x \in V$
169	6 8 1 2 9 4 19	imasmulval	$⊢ (φ \land \underset{˙}{1} \in V \land x \in V) \to F (\underset{˙}{1}) \cdot_{U} F (x) = F (\underset{˙}{1} \underset{˙}{\cdot} x)$
170	166 167 168 169	syl3anc	$⊢ (φ \land x \in V) \to F (\underset{˙}{1}) \cdot_{U} F (x) = F (\underset{˙}{1} \underset{˙}{\cdot} x)$
171	2	eleq2d	$⊢ φ \to (x \in V \leftrightarrow x \in {Base}_{R})$
172	171	biimpa	$⊢ (φ \land x \in V) \to x \in {Base}_{R}$
173	26 4 5	ringlidm	$⊢ (R \in Ring \land x \in {Base}_{R}) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
174	9 172 173	syl2an2r	$⊢ (φ \land x \in V) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
175	174	fveq2d	$⊢ (φ \land x \in V) \to F (\underset{˙}{1} \underset{˙}{\cdot} x) = F (x)$
176	170 175	eqtrd	$⊢ (φ \land x \in V) \to F (\underset{˙}{1}) \cdot_{U} F (x) = F (x)$
177		oveq2	$⊢ F (x) = u \to F (\underset{˙}{1}) \cdot_{U} F (x) = F (\underset{˙}{1}) \cdot_{U} u$
178		id	$⊢ F (x) = u \to F (x) = u$
179	177 178	eqeq12d	$⊢ F (x) = u \to (F (\underset{˙}{1}) \cdot_{U} F (x) = F (x) \leftrightarrow F (\underset{˙}{1}) \cdot_{U} u = u)$
180	176 179	syl5ibcom	$⊢ (φ \land x \in V) \to (F (x) = u \to F (\underset{˙}{1}) \cdot_{U} u = u)$
181	180	rexlimdva	$⊢ φ \to (\exists x \in V F (x) = u \to F (\underset{˙}{1}) \cdot_{U} u = u)$
182	165 181	sylbid	$⊢ φ \to (u \in B \to F (\underset{˙}{1}) \cdot_{U} u = u)$
183	182	imp	$⊢ (φ \land u \in B) \to F (\underset{˙}{1}) \cdot_{U} u = u$
184	6 8 1 2 9 4 19	imasmulval	$⊢ (φ \land x \in V \land \underset{˙}{1} \in V) \to F (x) \cdot_{U} F (\underset{˙}{1}) = F (x \underset{˙}{\cdot} \underset{˙}{1})$
185	167 184	mpd3an3	$⊢ (φ \land x \in V) \to F (x) \cdot_{U} F (\underset{˙}{1}) = F (x \underset{˙}{\cdot} \underset{˙}{1})$
186	26 4 5	ringridm	$⊢ (R \in Ring \land x \in {Base}_{R}) \to x \underset{˙}{\cdot} \underset{˙}{1} = x$
187	9 172 186	syl2an2r	$⊢ (φ \land x \in V) \to x \underset{˙}{\cdot} \underset{˙}{1} = x$
188	187	fveq2d	$⊢ (φ \land x \in V) \to F (x \underset{˙}{\cdot} \underset{˙}{1}) = F (x)$
189	185 188	eqtrd	$⊢ (φ \land x \in V) \to F (x) \cdot_{U} F (\underset{˙}{1}) = F (x)$
190		oveq1	$⊢ F (x) = u \to F (x) \cdot_{U} F (\underset{˙}{1}) = u \cdot_{U} F (\underset{˙}{1})$
191	190 178	eqeq12d	$⊢ F (x) = u \to (F (x) \cdot_{U} F (\underset{˙}{1}) = F (x) \leftrightarrow u \cdot_{U} F (\underset{˙}{1}) = u)$
192	189 191	syl5ibcom	$⊢ (φ \land x \in V) \to (F (x) = u \to u \cdot_{U} F (\underset{˙}{1}) = u)$
193	192	rexlimdva	$⊢ φ \to (\exists x \in V F (x) = u \to u \cdot_{U} F (\underset{˙}{1}) = u)$
194	165 193	sylbid	$⊢ φ \to (u \in B \to u \cdot_{U} F (\underset{˙}{1}) = u)$
195	194	imp	$⊢ (φ \land u \in B) \to u \cdot_{U} F (\underset{˙}{1}) = u$
196	10 11 12 18 33 96 131 157 163 183 195	isringd	$⊢ φ \to U \in Ring$
197	163 10	eleqtrd	$⊢ φ \to F (\underset{˙}{1}) \in {Base}_{U}$
198	10	eleq2d	$⊢ φ \to (u \in B \leftrightarrow u \in {Base}_{U})$
199	182 194	jcad	$⊢ φ \to (u \in B \to (F (\underset{˙}{1}) \cdot_{U} u = u \land u \cdot_{U} F (\underset{˙}{1}) = u))$
200	198 199	sylbird	$⊢ φ \to (u \in {Base}_{U} \to (F (\underset{˙}{1}) \cdot_{U} u = u \land u \cdot_{U} F (\underset{˙}{1}) = u))$
201	200	ralrimiv	$⊢ φ \to \forall u \in {Base}_{U} (F (\underset{˙}{1}) \cdot_{U} u = u \land u \cdot_{U} F (\underset{˙}{1}) = u)$
202		eqid	$⊢ {Base}_{U} = {Base}_{U}$
203		eqid	$⊢ 1_{U} = 1_{U}$
204	202 19 203	isringid	$⊢ U \in Ring \to ((F (\underset{˙}{1}) \in {Base}_{U} \land \forall u \in {Base}_{U} (F (\underset{˙}{1}) \cdot_{U} u = u \land u \cdot_{U} F (\underset{˙}{1}) = u)) \leftrightarrow 1_{U} = F (\underset{˙}{1}))$
205	196 204	syl	$⊢ φ \to ((F (\underset{˙}{1}) \in {Base}_{U} \land \forall u \in {Base}_{U} (F (\underset{˙}{1}) \cdot_{U} u = u \land u \cdot_{U} F (\underset{˙}{1}) = u)) \leftrightarrow 1_{U} = F (\underset{˙}{1}))$
206	197 201 205	mpbi2and	$⊢ φ \to 1_{U} = F (\underset{˙}{1})$
207	206	eqcomd	$⊢ φ \to F (\underset{˙}{1}) = 1_{U}$
208	196 207	jca	$⊢ φ \to (U \in Ring \land F (\underset{˙}{1}) = 1_{U})$

Metamath Proof Explorer

Theorem imasring

Proof