This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imaslmod

Description: The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023)

Ref Expression
Hypotheses imaslmod.u 
|- ( ph -> N = ( F "s M ) )
imaslmod.v 
|- V = ( Base ` M )
imaslmod.k 
|- S = ( Base ` ( Scalar ` M ) )
imaslmod.p 
|- .+ = ( +g ` M )
imaslmod.t 
|- .x. = ( .s ` M )
imaslmod.o 
|- .0. = ( 0g ` M )
imaslmod.f 
|- ( ph -> F : V -onto-> B )
imaslmod.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 ) ) ) )
imaslmod.e2 
|- ( ( ph /\ ( k e. S /\ a e. V /\ b e. V ) ) -> ( ( F ` a ) = ( F ` b ) -> ( F ` ( k .x. a ) ) = ( F ` ( k .x. b ) ) ) )
imaslmod.l 
|- ( ph -> M e. LMod )
Assertion imaslmod 
|- ( ph -> N e. LMod )

Proof

Step Hyp Ref Expression
1 imaslmod.u 
 |-  ( ph -> N = ( F "s M ) )
2 imaslmod.v 
 |-  V = ( Base ` M )
3 imaslmod.k 
 |-  S = ( Base ` ( Scalar ` M ) )
4 imaslmod.p 
 |-  .+ = ( +g ` M )
5 imaslmod.t 
 |-  .x. = ( .s ` M )
6 imaslmod.o 
 |-  .0. = ( 0g ` M )
7 imaslmod.f 
 |-  ( ph -> F : V -onto-> B )
8 imaslmod.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 ) ) ) )
9 imaslmod.e2 
 |-  ( ( ph /\ ( k e. S /\ a e. V /\ b e. V ) ) -> ( ( F ` a ) = ( F ` b ) -> ( F ` ( k .x. a ) ) = ( F ` ( k .x. b ) ) ) )
10 imaslmod.l 
 |-  ( ph -> M e. LMod )
11 2 a1i 
 |-  ( ph -> V = ( Base ` M ) )
12 1 11 7 10 imasbas 
 |-  ( ph -> B = ( Base ` N ) )
13 eqidd 
 |-  ( ph -> ( +g ` N ) = ( +g ` N ) )
14 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
15 1 11 7 10 14 imassca 
 |-  ( ph -> ( Scalar ` M ) = ( Scalar ` N ) )
16 eqidd 
 |-  ( ph -> ( .s ` N ) = ( .s ` N ) )
17 3 a1i 
 |-  ( ph -> S = ( Base ` ( Scalar ` M ) ) )
18 eqidd 
 |-  ( ph -> ( +g ` ( Scalar ` M ) ) = ( +g ` ( Scalar ` M ) ) )
19 eqidd 
 |-  ( ph -> ( .r ` ( Scalar ` M ) ) = ( .r ` ( Scalar ` M ) ) )
20 eqidd 
 |-  ( ph -> ( 1r ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) )
21 14 lmodring 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Ring )
22 10 21 syl 
 |-  ( ph -> ( Scalar ` M ) e. Ring )
23 4 a1i 
 |-  ( ph -> .+ = ( +g ` M ) )
24 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
25 10 24 syl 
 |-  ( ph -> M e. Grp )
26 1 11 23 7 8 25 6 imasgrp 
 |-  ( ph -> ( N e. Grp /\ ( F ` .0. ) = ( 0g ` N ) ) )
27 26 simpld 
 |-  ( ph -> N e. Grp )
28 eqid 
 |-  ( .s ` N ) = ( .s ` N )
29 10 adantr 
 |-  ( ( ph /\ ( k e. S /\ b e. V ) ) -> M e. LMod )
30 simprl 
 |-  ( ( ph /\ ( k e. S /\ b e. V ) ) -> k e. S )
31 simprr 
 |-  ( ( ph /\ ( k e. S /\ b e. V ) ) -> b e. V )
32 2 14 5 3 lmodvscl 
 |-  ( ( M e. LMod /\ k e. S /\ b e. V ) -> ( k .x. b ) e. V )
33 29 30 31 32 syl3anc 
 |-  ( ( ph /\ ( k e. S /\ b e. V ) ) -> ( k .x. b ) e. V )
34 1 11 7 10 14 3 5 28 9 33 imasvscaf 
 |-  ( ph -> ( .s ` N ) : ( S X. B ) --> B )
35 34 fovcld 
 |-  ( ( ph /\ u e. S /\ v e. B ) -> ( u ( .s ` N ) v ) e. B )
36 simp-5l 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ph )
37 simpllr 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u e. S /\ v e. B /\ w e. B ) )
38 37 simp1d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> u e. S )
39 38 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> u e. S )
40 36 25 syl 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> M e. Grp )
41 simplr 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> y e. V )
42 simp-4r 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> z e. V )
43 2 4 grpcl 
 |-  ( ( M e. Grp /\ y e. V /\ z e. V ) -> ( y .+ z ) e. V )
44 40 41 42 43 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( y .+ z ) e. V )
45 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ u e. S /\ ( y .+ z ) e. V ) -> ( u ( .s ` N ) ( F ` ( y .+ z ) ) ) = ( F ` ( u .x. ( y .+ z ) ) ) )
46 36 39 44 45 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( F ` ( y .+ z ) ) ) = ( F ` ( u .x. ( y .+ z ) ) ) )
47 eqid 
 |-  ( +g ` N ) = ( +g ` N )
48 7 8 1 11 10 4 47 imasaddval 
 |-  ( ( ph /\ y e. V /\ z e. V ) -> ( ( F ` y ) ( +g ` N ) ( F ` z ) ) = ( F ` ( y .+ z ) ) )
49 36 41 42 48 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( ( F ` y ) ( +g ` N ) ( F ` z ) ) = ( F ` ( y .+ z ) ) )
50 simpr 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( F ` y ) = v )
51 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( F ` z ) = w )
52 50 51 oveq12d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( ( F ` y ) ( +g ` N ) ( F ` z ) ) = ( v ( +g ` N ) w ) )
53 49 52 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( F ` ( y .+ z ) ) = ( v ( +g ` N ) w ) )
54 53 oveq2d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( F ` ( y .+ z ) ) ) = ( u ( .s ` N ) ( v ( +g ` N ) w ) ) )
55 36 10 syl 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> M e. LMod )
56 2 4 14 5 3 lmodvsdi 
 |-  ( ( M e. LMod /\ ( u e. S /\ y e. V /\ z e. V ) ) -> ( u .x. ( y .+ z ) ) = ( ( u .x. y ) .+ ( u .x. z ) ) )
57 55 39 41 42 56 syl13anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u .x. ( y .+ z ) ) = ( ( u .x. y ) .+ ( u .x. z ) ) )
58 57 fveq2d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( F ` ( u .x. ( y .+ z ) ) ) = ( F ` ( ( u .x. y ) .+ ( u .x. z ) ) ) )
59 46 54 58 3eqtr3d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( v ( +g ` N ) w ) ) = ( F ` ( ( u .x. y ) .+ ( u .x. z ) ) ) )
60 2 14 5 3 lmodvscl 
 |-  ( ( M e. LMod /\ u e. S /\ y e. V ) -> ( u .x. y ) e. V )
61 55 39 41 60 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u .x. y ) e. V )
62 2 14 5 3 lmodvscl 
 |-  ( ( M e. LMod /\ u e. S /\ z e. V ) -> ( u .x. z ) e. V )
63 55 39 42 62 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u .x. z ) e. V )
64 7 8 1 11 10 4 47 imasaddval 
 |-  ( ( ph /\ ( u .x. y ) e. V /\ ( u .x. z ) e. V ) -> ( ( F ` ( u .x. y ) ) ( +g ` N ) ( F ` ( u .x. z ) ) ) = ( F ` ( ( u .x. y ) .+ ( u .x. z ) ) ) )
65 36 61 63 64 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( ( F ` ( u .x. y ) ) ( +g ` N ) ( F ` ( u .x. z ) ) ) = ( F ` ( ( u .x. y ) .+ ( u .x. z ) ) ) )
66 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ u e. S /\ y e. V ) -> ( u ( .s ` N ) ( F ` y ) ) = ( F ` ( u .x. y ) ) )
67 36 39 41 66 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( F ` y ) ) = ( F ` ( u .x. y ) ) )
68 50 oveq2d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( F ` y ) ) = ( u ( .s ` N ) v ) )
69 67 68 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( F ` ( u .x. y ) ) = ( u ( .s ` N ) v ) )
70 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ u e. S /\ z e. V ) -> ( u ( .s ` N ) ( F ` z ) ) = ( F ` ( u .x. z ) ) )
71 36 39 42 70 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( F ` z ) ) = ( F ` ( u .x. z ) ) )
72 51 oveq2d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( F ` z ) ) = ( u ( .s ` N ) w ) )
73 71 72 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( F ` ( u .x. z ) ) = ( u ( .s ` N ) w ) )
74 69 73 oveq12d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( ( F ` ( u .x. y ) ) ( +g ` N ) ( F ` ( u .x. z ) ) ) = ( ( u ( .s ` N ) v ) ( +g ` N ) ( u ( .s ` N ) w ) ) )
75 59 65 74 3eqtr2d 
 |-  ( ( ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) /\ y e. V ) /\ ( F ` y ) = v ) -> ( u ( .s ` N ) ( v ( +g ` N ) w ) ) = ( ( u ( .s ` N ) v ) ( +g ` N ) ( u ( .s ` N ) w ) ) )
76 simplll 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ph )
77 37 simp2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> v e. B )
78 fofn 
 |-  ( F : V -onto-> B -> F Fn V )
79 7 78 syl 
 |-  ( ph -> F Fn V )
80 simpr 
 |-  ( ( ph /\ v e. B ) -> v e. B )
81 forn 
 |-  ( F : V -onto-> B -> ran F = B )
82 7 81 syl 
 |-  ( ph -> ran F = B )
83 82 adantr 
 |-  ( ( ph /\ v e. B ) -> ran F = B )
84 80 83 eleqtrrd 
 |-  ( ( ph /\ v e. B ) -> v e. ran F )
85 fvelrnb 
 |-  ( F Fn V -> ( v e. ran F <-> E. y e. V ( F ` y ) = v ) )
86 85 biimpa 
 |-  ( ( F Fn V /\ v e. ran F ) -> E. y e. V ( F ` y ) = v )
87 79 84 86 syl2an2r 
 |-  ( ( ph /\ v e. B ) -> E. y e. V ( F ` y ) = v )
88 76 77 87 syl2anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> E. y e. V ( F ` y ) = v )
89 75 88 r19.29a 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( .s ` N ) ( v ( +g ` N ) w ) ) = ( ( u ( .s ` N ) v ) ( +g ` N ) ( u ( .s ` N ) w ) ) )
90 simpr 
 |-  ( ( ph /\ w e. B ) -> w e. B )
91 82 adantr 
 |-  ( ( ph /\ w e. B ) -> ran F = B )
92 90 91 eleqtrrd 
 |-  ( ( ph /\ w e. B ) -> w e. ran F )
93 fvelrnb 
 |-  ( F Fn V -> ( w e. ran F <-> E. z e. V ( F ` z ) = w ) )
94 93 biimpa 
 |-  ( ( F Fn V /\ w e. ran F ) -> E. z e. V ( F ` z ) = w )
95 79 92 94 syl2an2r 
 |-  ( ( ph /\ w e. B ) -> E. z e. V ( F ` z ) = w )
96 95 3ad2antr3 
 |-  ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) -> E. z e. V ( F ` z ) = w )
97 89 96 r19.29a 
 |-  ( ( ph /\ ( u e. S /\ v e. B /\ w e. B ) ) -> ( u ( .s ` N ) ( v ( +g ` N ) w ) ) = ( ( u ( .s ` N ) v ) ( +g ` N ) ( u ( .s ` N ) w ) ) )
98 simplll 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ph )
99 10 ad3antrrr 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> M e. LMod )
100 simpllr 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u e. S /\ v e. S /\ w e. B ) )
101 100 simp1d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> u e. S )
102 100 simp2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> v e. S )
103 eqid 
 |-  ( +g ` ( Scalar ` M ) ) = ( +g ` ( Scalar ` M ) )
104 14 3 103 lmodacl 
 |-  ( ( M e. LMod /\ u e. S /\ v e. S ) -> ( u ( +g ` ( Scalar ` M ) ) v ) e. S )
105 99 101 102 104 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( +g ` ( Scalar ` M ) ) v ) e. S )
106 simplr 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> z e. V )
107 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ ( u ( +g ` ( Scalar ` M ) ) v ) e. S /\ z e. V ) -> ( ( u ( +g ` ( Scalar ` M ) ) v ) ( .s ` N ) ( F ` z ) ) = ( F ` ( ( u ( +g ` ( Scalar ` M ) ) v ) .x. z ) ) )
108 98 105 106 107 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( +g ` ( Scalar ` M ) ) v ) ( .s ` N ) ( F ` z ) ) = ( F ` ( ( u ( +g ` ( Scalar ` M ) ) v ) .x. z ) ) )
109 simpr 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( F ` z ) = w )
110 109 oveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( +g ` ( Scalar ` M ) ) v ) ( .s ` N ) ( F ` z ) ) = ( ( u ( +g ` ( Scalar ` M ) ) v ) ( .s ` N ) w ) )
111 2 4 14 5 3 103 lmodvsdir 
 |-  ( ( M e. LMod /\ ( u e. S /\ v e. S /\ z e. V ) ) -> ( ( u ( +g ` ( Scalar ` M ) ) v ) .x. z ) = ( ( u .x. z ) .+ ( v .x. z ) ) )
112 99 101 102 106 111 syl13anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( +g ` ( Scalar ` M ) ) v ) .x. z ) = ( ( u .x. z ) .+ ( v .x. z ) ) )
113 112 fveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( F ` ( ( u ( +g ` ( Scalar ` M ) ) v ) .x. z ) ) = ( F ` ( ( u .x. z ) .+ ( v .x. z ) ) ) )
114 99 101 106 62 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u .x. z ) e. V )
115 2 14 5 3 lmodvscl 
 |-  ( ( M e. LMod /\ v e. S /\ z e. V ) -> ( v .x. z ) e. V )
116 99 102 106 115 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( v .x. z ) e. V )
117 7 8 1 11 10 4 47 imasaddval 
 |-  ( ( ph /\ ( u .x. z ) e. V /\ ( v .x. z ) e. V ) -> ( ( F ` ( u .x. z ) ) ( +g ` N ) ( F ` ( v .x. z ) ) ) = ( F ` ( ( u .x. z ) .+ ( v .x. z ) ) ) )
118 98 114 116 117 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( F ` ( u .x. z ) ) ( +g ` N ) ( F ` ( v .x. z ) ) ) = ( F ` ( ( u .x. z ) .+ ( v .x. z ) ) ) )
119 98 101 106 70 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( .s ` N ) ( F ` z ) ) = ( F ` ( u .x. z ) ) )
120 109 oveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( .s ` N ) ( F ` z ) ) = ( u ( .s ` N ) w ) )
121 119 120 eqtr3d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( F ` ( u .x. z ) ) = ( u ( .s ` N ) w ) )
122 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ v e. S /\ z e. V ) -> ( v ( .s ` N ) ( F ` z ) ) = ( F ` ( v .x. z ) ) )
123 98 102 106 122 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( v ( .s ` N ) ( F ` z ) ) = ( F ` ( v .x. z ) ) )
124 109 oveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( v ( .s ` N ) ( F ` z ) ) = ( v ( .s ` N ) w ) )
125 123 124 eqtr3d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( F ` ( v .x. z ) ) = ( v ( .s ` N ) w ) )
126 121 125 oveq12d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( F ` ( u .x. z ) ) ( +g ` N ) ( F ` ( v .x. z ) ) ) = ( ( u ( .s ` N ) w ) ( +g ` N ) ( v ( .s ` N ) w ) ) )
127 113 118 126 3eqtr2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( F ` ( ( u ( +g ` ( Scalar ` M ) ) v ) .x. z ) ) = ( ( u ( .s ` N ) w ) ( +g ` N ) ( v ( .s ` N ) w ) ) )
128 108 110 127 3eqtr3d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( +g ` ( Scalar ` M ) ) v ) ( .s ` N ) w ) = ( ( u ( .s ` N ) w ) ( +g ` N ) ( v ( .s ` N ) w ) ) )
129 95 3ad2antr3 
 |-  ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) -> E. z e. V ( F ` z ) = w )
130 128 129 r19.29a 
 |-  ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) -> ( ( u ( +g ` ( Scalar ` M ) ) v ) ( .s ` N ) w ) = ( ( u ( .s ` N ) w ) ( +g ` N ) ( v ( .s ` N ) w ) ) )
131 eqid 
 |-  ( .r ` ( Scalar ` M ) ) = ( .r ` ( Scalar ` M ) )
132 14 3 131 lmodmcl 
 |-  ( ( M e. LMod /\ u e. S /\ v e. S ) -> ( u ( .r ` ( Scalar ` M ) ) v ) e. S )
133 99 101 102 132 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( .r ` ( Scalar ` M ) ) v ) e. S )
134 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ ( u ( .r ` ( Scalar ` M ) ) v ) e. S /\ z e. V ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) ( .s ` N ) ( F ` z ) ) = ( F ` ( ( u ( .r ` ( Scalar ` M ) ) v ) .x. z ) ) )
135 98 133 106 134 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) ( .s ` N ) ( F ` z ) ) = ( F ` ( ( u ( .r ` ( Scalar ` M ) ) v ) .x. z ) ) )
136 109 oveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) ( .s ` N ) ( F ` z ) ) = ( ( u ( .r ` ( Scalar ` M ) ) v ) ( .s ` N ) w ) )
137 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ u e. S /\ ( v .x. z ) e. V ) -> ( u ( .s ` N ) ( F ` ( v .x. z ) ) ) = ( F ` ( u .x. ( v .x. z ) ) ) )
138 98 101 116 137 syl3anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( .s ` N ) ( F ` ( v .x. z ) ) ) = ( F ` ( u .x. ( v .x. z ) ) ) )
139 123 oveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( .s ` N ) ( v ( .s ` N ) ( F ` z ) ) ) = ( u ( .s ` N ) ( F ` ( v .x. z ) ) ) )
140 2 14 5 3 131 lmodvsass 
 |-  ( ( M e. LMod /\ ( u e. S /\ v e. S /\ z e. V ) ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) .x. z ) = ( u .x. ( v .x. z ) ) )
141 99 101 102 106 140 syl13anc 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) .x. z ) = ( u .x. ( v .x. z ) ) )
142 141 fveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( F ` ( ( u ( .r ` ( Scalar ` M ) ) v ) .x. z ) ) = ( F ` ( u .x. ( v .x. z ) ) ) )
143 138 139 142 3eqtr4rd 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( F ` ( ( u ( .r ` ( Scalar ` M ) ) v ) .x. z ) ) = ( u ( .s ` N ) ( v ( .s ` N ) ( F ` z ) ) ) )
144 135 136 143 3eqtr3d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) ( .s ` N ) w ) = ( u ( .s ` N ) ( v ( .s ` N ) ( F ` z ) ) ) )
145 124 oveq2d 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( u ( .s ` N ) ( v ( .s ` N ) ( F ` z ) ) ) = ( u ( .s ` N ) ( v ( .s ` N ) w ) ) )
146 144 145 eqtrd 
 |-  ( ( ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) /\ z e. V ) /\ ( F ` z ) = w ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) ( .s ` N ) w ) = ( u ( .s ` N ) ( v ( .s ` N ) w ) ) )
147 146 129 r19.29a 
 |-  ( ( ph /\ ( u e. S /\ v e. S /\ w e. B ) ) -> ( ( u ( .r ` ( Scalar ` M ) ) v ) ( .s ` N ) w ) = ( u ( .s ` N ) ( v ( .s ` N ) w ) ) )
148 simplll 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ph )
149 eqid 
 |-  ( 1r ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) )
150 3 149 ringidcl 
 |-  ( ( Scalar ` M ) e. Ring -> ( 1r ` ( Scalar ` M ) ) e. S )
151 22 150 syl 
 |-  ( ph -> ( 1r ` ( Scalar ` M ) ) e. S )
152 151 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( 1r ` ( Scalar ` M ) ) e. S )
153 simplr 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> x e. V )
154 1 11 7 10 14 3 5 28 9 imasvscaval 
 |-  ( ( ph /\ ( 1r ` ( Scalar ` M ) ) e. S /\ x e. V ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` N ) ( F ` x ) ) = ( F ` ( ( 1r ` ( Scalar ` M ) ) .x. x ) ) )
155 148 152 153 154 syl3anc 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` N ) ( F ` x ) ) = ( F ` ( ( 1r ` ( Scalar ` M ) ) .x. x ) ) )
156 simpr 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( F ` x ) = u )
157 156 oveq2d 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` N ) ( F ` x ) ) = ( ( 1r ` ( Scalar ` M ) ) ( .s ` N ) u ) )
158 10 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> M e. LMod )
159 2 14 5 149 lmodvs1 
 |-  ( ( M e. LMod /\ x e. V ) -> ( ( 1r ` ( Scalar ` M ) ) .x. x ) = x )
160 158 153 159 syl2anc 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( ( 1r ` ( Scalar ` M ) ) .x. x ) = x )
161 160 fveq2d 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( F ` ( ( 1r ` ( Scalar ` M ) ) .x. x ) ) = ( F ` x ) )
162 161 156 eqtrd 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( F ` ( ( 1r ` ( Scalar ` M ) ) .x. x ) ) = u )
163 155 157 162 3eqtr3d 
 |-  ( ( ( ( ph /\ u e. B ) /\ x e. V ) /\ ( F ` x ) = u ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` N ) u ) = u )
164 simpr 
 |-  ( ( ph /\ u e. B ) -> u e. B )
165 82 adantr 
 |-  ( ( ph /\ u e. B ) -> ran F = B )
166 164 165 eleqtrrd 
 |-  ( ( ph /\ u e. B ) -> u e. ran F )
167 fvelrnb 
 |-  ( F Fn V -> ( u e. ran F <-> E. x e. V ( F ` x ) = u ) )
168 167 biimpa 
 |-  ( ( F Fn V /\ u e. ran F ) -> E. x e. V ( F ` x ) = u )
169 79 166 168 syl2an2r 
 |-  ( ( ph /\ u e. B ) -> E. x e. V ( F ` x ) = u )
170 163 169 r19.29a 
 |-  ( ( ph /\ u e. B ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` N ) u ) = u )
171 12 13 15 16 17 18 19 20 22 27 35 97 130 147 170 islmodd 
 |-  ( ph -> N e. LMod )