Metamath Proof Explorer

Theorem imasrng

Description: The image structure of a non-unital ring is a non-unital ring ( imasring analog). (Contributed by AV, 22-Feb-2025)

Ref Expression
Hypotheses imasrng.u 
|- ( ph -> U = ( F "s R ) )
imasrng.v 
|- ( ph -> V = ( Base ` R ) )
imasrng.p 
|- .+ = ( +g ` R )
imasrng.t 
|- .x. = ( .r ` R )
imasrng.f 
|- ( ph -> F : V -onto-> B )
imasrng.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 ) ) ) )
imasrng.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 ) ) ) )
imasrng.r 
|- ( ph -> R e. Rng )
Assertion imasrng 
|- ( ph -> U e. Rng )

Proof

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