Step |
Hyp |
Ref |
Expression |
1 |
|
imasmnd.u |
|- ( ph -> U = ( F "s R ) ) |
2 |
|
imasmnd.v |
|- ( ph -> V = ( Base ` R ) ) |
3 |
|
imasmnd.p |
|- .+ = ( +g ` R ) |
4 |
|
imasmnd.f |
|- ( ph -> F : V -onto-> B ) |
5 |
|
imasmnd.e |
|- ( ( 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 ) ) ) ) |
6 |
|
imasmnd2.r |
|- ( ph -> R e. W ) |
7 |
|
imasmnd2.1 |
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V ) |
8 |
|
imasmnd2.2 |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) ) |
9 |
|
imasmnd2.3 |
|- ( ph -> .0. e. V ) |
10 |
|
imasmnd2.4 |
|- ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) ) |
11 |
|
imasmnd2.5 |
|- ( ( ph /\ x e. V ) -> ( F ` ( x .+ .0. ) ) = ( F ` x ) ) |
12 |
1 2 4 6
|
imasbas |
|- ( ph -> B = ( Base ` U ) ) |
13 |
|
eqidd |
|- ( ph -> ( +g ` U ) = ( +g ` U ) ) |
14 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
15 |
7
|
3expb |
|- ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. V ) |
16 |
15
|
caovclg |
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .+ q ) e. V ) |
17 |
4 5 1 2 6 3 14 16
|
imasaddf |
|- ( ph -> ( +g ` U ) : ( B X. B ) --> B ) |
18 |
|
fovrn |
|- ( ( ( +g ` U ) : ( B X. B ) --> B /\ u e. B /\ v e. B ) -> ( u ( +g ` U ) v ) e. B ) |
19 |
17 18
|
syl3an1 |
|- ( ( ph /\ u e. B /\ v e. B ) -> ( u ( +g ` U ) v ) e. B ) |
20 |
|
forn |
|- ( F : V -onto-> B -> ran F = B ) |
21 |
4 20
|
syl |
|- ( ph -> ran F = B ) |
22 |
21
|
eleq2d |
|- ( ph -> ( u e. ran F <-> u e. B ) ) |
23 |
21
|
eleq2d |
|- ( ph -> ( v e. ran F <-> v e. B ) ) |
24 |
21
|
eleq2d |
|- ( ph -> ( w e. ran F <-> w e. B ) ) |
25 |
22 23 24
|
3anbi123d |
|- ( ph -> ( ( u e. ran F /\ v e. ran F /\ w e. ran F ) <-> ( u e. B /\ v e. B /\ w e. B ) ) ) |
26 |
|
fofn |
|- ( F : V -onto-> B -> F Fn V ) |
27 |
4 26
|
syl |
|- ( ph -> F Fn V ) |
28 |
|
fvelrnb |
|- ( F Fn V -> ( u e. ran F <-> E. x e. V ( F ` x ) = u ) ) |
29 |
|
fvelrnb |
|- ( F Fn V -> ( v e. ran F <-> E. y e. V ( F ` y ) = v ) ) |
30 |
|
fvelrnb |
|- ( F Fn V -> ( w e. ran F <-> E. z e. V ( F ` z ) = w ) ) |
31 |
28 29 30
|
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 ) ) ) |
32 |
27 31
|
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 ) ) ) |
33 |
25 32
|
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 ) ) ) |
34 |
|
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 ) ) |
35 |
33 34
|
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 ) ) ) |
36 |
|
simpl |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ph ) |
37 |
7
|
3adant3r3 |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( x .+ y ) e. V ) |
38 |
|
simpr3 |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> z e. V ) |
39 |
4 5 1 2 6 3 14
|
imasaddval |
|- ( ( ph /\ ( x .+ y ) e. V /\ z e. V ) -> ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) = ( F ` ( ( x .+ y ) .+ z ) ) ) |
40 |
36 37 38 39
|
syl3anc |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) = ( F ` ( ( x .+ y ) .+ z ) ) ) |
41 |
|
simpr1 |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> x e. V ) |
42 |
16
|
caovclg |
|- ( ( ph /\ ( y e. V /\ z e. V ) ) -> ( y .+ z ) e. V ) |
43 |
42
|
3adantr1 |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( y .+ z ) e. V ) |
44 |
4 5 1 2 6 3 14
|
imasaddval |
|- ( ( ph /\ x e. V /\ ( y .+ z ) e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) = ( F ` ( x .+ ( y .+ z ) ) ) ) |
45 |
36 41 43 44
|
syl3anc |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) = ( F ` ( x .+ ( y .+ z ) ) ) ) |
46 |
8 40 45
|
3eqtr4d |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) ) |
47 |
4 5 1 2 6 3 14
|
imasaddval |
|- ( ( ph /\ x e. V /\ y e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` y ) ) = ( F ` ( x .+ y ) ) ) |
48 |
47
|
3adant3r3 |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` x ) ( +g ` U ) ( F ` y ) ) = ( F ` ( x .+ y ) ) ) |
49 |
48
|
oveq1d |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) ) |
50 |
4 5 1 2 6 3 14
|
imasaddval |
|- ( ( ph /\ y e. V /\ z e. V ) -> ( ( F ` y ) ( +g ` U ) ( F ` z ) ) = ( F ` ( y .+ z ) ) ) |
51 |
50
|
3adant3r1 |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` y ) ( +g ` U ) ( F ` z ) ) = ( F ` ( y .+ z ) ) ) |
52 |
51
|
oveq2d |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) = ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) ) |
53 |
46 49 52
|
3eqtr4d |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) ) |
54 |
|
simp1 |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( F ` x ) = u ) |
55 |
|
simp2 |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( F ` y ) = v ) |
56 |
54 55
|
oveq12d |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( F ` x ) ( +g ` U ) ( F ` y ) ) = ( u ( +g ` U ) v ) ) |
57 |
|
simp3 |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( F ` z ) = w ) |
58 |
56 57
|
oveq12d |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( u ( +g ` U ) v ) ( +g ` U ) w ) ) |
59 |
55 57
|
oveq12d |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( F ` y ) ( +g ` U ) ( F ` z ) ) = ( v ( +g ` U ) w ) ) |
60 |
54 59
|
oveq12d |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) |
61 |
58 60
|
eqeq12d |
|- ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) <-> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) |
62 |
53 61
|
syl5ibcom |
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) |
63 |
62
|
3exp2 |
|- ( ph -> ( x e. V -> ( y e. V -> ( z e. V -> ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) ) ) ) |
64 |
63
|
imp32 |
|- ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( z e. V -> ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) ) |
65 |
64
|
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 ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) |
66 |
65
|
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 ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) |
67 |
35 66
|
sylbid |
|- ( ph -> ( ( u e. B /\ v e. B /\ w e. B ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) |
68 |
67
|
imp |
|- ( ( ph /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) |
69 |
|
fof |
|- ( F : V -onto-> B -> F : V --> B ) |
70 |
4 69
|
syl |
|- ( ph -> F : V --> B ) |
71 |
70 9
|
ffvelrnd |
|- ( ph -> ( F ` .0. ) e. B ) |
72 |
27 28
|
syl |
|- ( ph -> ( u e. ran F <-> E. x e. V ( F ` x ) = u ) ) |
73 |
22 72
|
bitr3d |
|- ( ph -> ( u e. B <-> E. x e. V ( F ` x ) = u ) ) |
74 |
|
simpl |
|- ( ( ph /\ x e. V ) -> ph ) |
75 |
9
|
adantr |
|- ( ( ph /\ x e. V ) -> .0. e. V ) |
76 |
|
simpr |
|- ( ( ph /\ x e. V ) -> x e. V ) |
77 |
4 5 1 2 6 3 14
|
imasaddval |
|- ( ( ph /\ .0. e. V /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` ( .0. .+ x ) ) ) |
78 |
74 75 76 77
|
syl3anc |
|- ( ( ph /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` ( .0. .+ x ) ) ) |
79 |
78 10
|
eqtrd |
|- ( ( ph /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` x ) ) |
80 |
|
oveq2 |
|- ( ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( ( F ` .0. ) ( +g ` U ) u ) ) |
81 |
|
id |
|- ( ( F ` x ) = u -> ( F ` x ) = u ) |
82 |
80 81
|
eqeq12d |
|- ( ( F ` x ) = u -> ( ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` x ) <-> ( ( F ` .0. ) ( +g ` U ) u ) = u ) ) |
83 |
79 82
|
syl5ibcom |
|- ( ( ph /\ x e. V ) -> ( ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) ) |
84 |
83
|
rexlimdva |
|- ( ph -> ( E. x e. V ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) ) |
85 |
73 84
|
sylbid |
|- ( ph -> ( u e. B -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) ) |
86 |
85
|
imp |
|- ( ( ph /\ u e. B ) -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) |
87 |
4 5 1 2 6 3 14
|
imasaddval |
|- ( ( ph /\ x e. V /\ .0. e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` ( x .+ .0. ) ) ) |
88 |
75 87
|
mpd3an3 |
|- ( ( ph /\ x e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` ( x .+ .0. ) ) ) |
89 |
88 11
|
eqtrd |
|- ( ( ph /\ x e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` x ) ) |
90 |
|
oveq1 |
|- ( ( F ` x ) = u -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( u ( +g ` U ) ( F ` .0. ) ) ) |
91 |
90 81
|
eqeq12d |
|- ( ( F ` x ) = u -> ( ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` x ) <-> ( u ( +g ` U ) ( F ` .0. ) ) = u ) ) |
92 |
89 91
|
syl5ibcom |
|- ( ( ph /\ x e. V ) -> ( ( F ` x ) = u -> ( u ( +g ` U ) ( F ` .0. ) ) = u ) ) |
93 |
92
|
rexlimdva |
|- ( ph -> ( E. x e. V ( F ` x ) = u -> ( u ( +g ` U ) ( F ` .0. ) ) = u ) ) |
94 |
73 93
|
sylbid |
|- ( ph -> ( u e. B -> ( u ( +g ` U ) ( F ` .0. ) ) = u ) ) |
95 |
94
|
imp |
|- ( ( ph /\ u e. B ) -> ( u ( +g ` U ) ( F ` .0. ) ) = u ) |
96 |
12 13 19 68 71 86 95
|
ismndd |
|- ( ph -> U e. Mnd ) |
97 |
12 13 71 86 95
|
grpidd |
|- ( ph -> ( F ` .0. ) = ( 0g ` U ) ) |
98 |
96 97
|
jca |
|- ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) ) |