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 ) ) )