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
|- ( ph -> U = ( F "s R ) )
imasring.v
|- ( ph -> V = ( Base ` R ) )
imasring.p
|- .+ = ( +g ` R )
imasring.t
|- .x. = ( .r ` R )
imasring.o
|- .1. = ( 1r ` R )
imasring.f
|- ( ph -> F : V -onto-> B )
imasring.e1
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imasring.e2
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
imasring.r
|- ( ph -> R e. Ring )
Assertion imasring
|- ( ph -> ( U e. Ring /\ ( F ` .1. ) = ( 1r ` U ) ) )

Proof

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