Metamath Proof Explorer

Theorem frlmphllem

Description: Lemma for frlmphl . (Contributed by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmphl.y 
|- Y = ( R freeLMod I )
frlmphl.b 
|- B = ( Base ` R )
frlmphl.t 
|- .x. = ( .r ` R )
frlmphl.v 
|- V = ( Base ` Y )
frlmphl.j 
|- ., = ( .i ` Y )
frlmphl.o 
|- O = ( 0g ` Y )
frlmphl.0 
|- .0. = ( 0g ` R )
frlmphl.s 
|- .* = ( *r ` R )
frlmphl.f 
|- ( ph -> R e. Field )
frlmphl.m 
|- ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) -> g = O )
frlmphl.u 
|- ( ( ph /\ x e. B ) -> ( .* ` x ) = x )
frlmphl.i 
|- ( ph -> I e. W )
Assertion frlmphllem 
|- ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) finSupp .0. )

Proof

Step Hyp Ref Expression
1 frlmphl.y 
 |-  Y = ( R freeLMod I )
2 frlmphl.b 
 |-  B = ( Base ` R )
3 frlmphl.t 
 |-  .x. = ( .r ` R )
4 frlmphl.v 
 |-  V = ( Base ` Y )
5 frlmphl.j 
 |-  ., = ( .i ` Y )
6 frlmphl.o 
 |-  O = ( 0g ` Y )
7 frlmphl.0 
 |-  .0. = ( 0g ` R )
8 frlmphl.s 
 |-  .* = ( *r ` R )
9 frlmphl.f 
 |-  ( ph -> R e. Field )
10 frlmphl.m 
 |-  ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) -> g = O )
11 frlmphl.u 
 |-  ( ( ph /\ x e. B ) -> ( .* ` x ) = x )
12 frlmphl.i 
 |-  ( ph -> I e. W )
13 12 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> I e. W )
14 simp2 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g e. V )
15 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ g e. V ) -> g e. ( B ^m I ) )
16 13 14 15 syl2anc 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g e. ( B ^m I ) )
17 elmapi 
 |-  ( g e. ( B ^m I ) -> g : I --> B )
18 16 17 syl 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g : I --> B )
19 18 ffnd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g Fn I )
20 simp3 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h e. V )
21 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ h e. V ) -> h e. ( B ^m I ) )
22 13 20 21 syl2anc 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h e. ( B ^m I ) )
23 elmapi 
 |-  ( h e. ( B ^m I ) -> h : I --> B )
24 22 23 syl 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h : I --> B )
25 24 ffnd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h Fn I )
26 inidm 
 |-  ( I i^i I ) = I
27 eqidd 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
28 eqidd 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
29 19 25 13 13 26 27 28 offval 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
30 29 oveq1d 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( ( g oF .x. h ) supp .0. ) = ( ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) supp .0. ) )
31 ovexd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( g oF .x. h ) e. _V )
32 funmpt 
 |-  Fun ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) )
33 funeq 
 |-  ( ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) -> ( Fun ( g oF .x. h ) <-> Fun ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
34 32 33 mpbiri 
 |-  ( ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) -> Fun ( g oF .x. h ) )
35 29 34 syl 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> Fun ( g oF .x. h ) )
36 1 7 4 frlmbasfsupp 
 |-  ( ( I e. W /\ g e. V ) -> g finSupp .0. )
37 13 14 36 syl2anc 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g finSupp .0. )
38 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
39 9 38 sylib 
 |-  ( ph -> ( R e. DivRing /\ R e. CRing ) )
40 39 simpld 
 |-  ( ph -> R e. DivRing )
41 drngring 
 |-  ( R e. DivRing -> R e. Ring )
42 40 41 syl 
 |-  ( ph -> R e. Ring )
43 42 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> R e. Ring )
44 2 7 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
45 43 44 syl 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> .0. e. B )
46 2 3 7 ringlz 
 |-  ( ( R e. Ring /\ x e. B ) -> ( .0. .x. x ) = .0. )
47 43 46 sylan 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. B ) -> ( .0. .x. x ) = .0. )
48 13 45 18 24 47 suppofss1d 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( ( g oF .x. h ) supp .0. ) C_ ( g supp .0. ) )
49 fsuppsssupp 
 |-  ( ( ( ( g oF .x. h ) e. _V /\ Fun ( g oF .x. h ) ) /\ ( g finSupp .0. /\ ( ( g oF .x. h ) supp .0. ) C_ ( g supp .0. ) ) ) -> ( g oF .x. h ) finSupp .0. )
50 49 fsuppimpd 
 |-  ( ( ( ( g oF .x. h ) e. _V /\ Fun ( g oF .x. h ) ) /\ ( g finSupp .0. /\ ( ( g oF .x. h ) supp .0. ) C_ ( g supp .0. ) ) ) -> ( ( g oF .x. h ) supp .0. ) e. Fin )
51 31 35 37 48 50 syl22anc 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( ( g oF .x. h ) supp .0. ) e. Fin )
52 30 51 eqeltrrd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) supp .0. ) e. Fin )
53 13 mptexd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) e. _V )
54 45 elexd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> .0. e. _V )
55 funisfsupp 
 |-  ( ( Fun ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) /\ ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) e. _V /\ .0. e. _V ) -> ( ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) finSupp .0. <-> ( ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) supp .0. ) e. Fin ) )
56 32 53 54 55 mp3an2i 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) finSupp .0. <-> ( ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) supp .0. ) e. Fin ) )
57 52 56 mpbird 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) finSupp .0. )