Metamath Proof Explorer

Theorem lincresunit3lem1

Description: Lemma 1 for lincresunit3 . (Contributed by AV, 17-May-2019)

Ref Expression
Hypotheses lincresunit.b 
|- B = ( Base ` M )
lincresunit.r 
|- R = ( Scalar ` M )
lincresunit.e 
|- E = ( Base ` R )
lincresunit.u 
|- U = ( Unit ` R )
lincresunit.0 
|- .0. = ( 0g ` R )
lincresunit.z 
|- Z = ( 0g ` M )
lincresunit.n 
|- N = ( invg ` R )
lincresunit.i 
|- I = ( invr ` R )
lincresunit.t 
|- .x. = ( .r ` R )
lincresunit.g 
|- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )
Assertion lincresunit3lem1 
|- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) = ( ( F ` z ) ( .s ` M ) z ) )

Proof

Step Hyp Ref Expression
1 lincresunit.b 
 |-  B = ( Base ` M )
2 lincresunit.r 
 |-  R = ( Scalar ` M )
3 lincresunit.e 
 |-  E = ( Base ` R )
4 lincresunit.u 
 |-  U = ( Unit ` R )
5 lincresunit.0 
 |-  .0. = ( 0g ` R )
6 lincresunit.z 
 |-  Z = ( 0g ` M )
7 lincresunit.n 
 |-  N = ( invg ` R )
8 lincresunit.i 
 |-  I = ( invr ` R )
9 lincresunit.t 
 |-  .x. = ( .r ` R )
10 lincresunit.g 
 |-  G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )
11 fveq2 
 |-  ( s = z -> ( F ` s ) = ( F ` z ) )
12 11 oveq2d 
 |-  ( s = z -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) = ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) )
13 simpr3 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> z e. ( S \ { X } ) )
14 ovexd 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) e. _V )
15 10 12 13 14 fvmptd3 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( G ` z ) = ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) )
16 15 oveq1d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( G ` z ) ( .s ` M ) z ) = ( ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ( .s ` M ) z ) )
17 16 oveq2d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ( .s ` M ) z ) ) )
18 simp2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> M e. LMod )
19 18 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> M e. LMod )
20 2 lmodfgrp 
 |-  ( M e. LMod -> R e. Grp )
21 20 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> R e. Grp )
22 3 4 unitcl 
 |-  ( ( F ` X ) e. U -> ( F ` X ) e. E )
23 22 3ad2ant2 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> ( F ` X ) e. E )
24 3 7 grpinvcl 
 |-  ( ( R e. Grp /\ ( F ` X ) e. E ) -> ( N ` ( F ` X ) ) e. E )
25 21 23 24 syl2an 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( N ` ( F ` X ) ) e. E )
26 3simpa 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) )
27 26 anim2i 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) )
28 eldifi 
 |-  ( z e. ( S \ { X } ) -> z e. S )
29 28 3ad2ant3 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> z e. S )
30 29 adantl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> z e. S )
31 1 2 3 4 5 6 7 8 9 10 lincresunitlem2 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ z e. S ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) e. E )
32 27 30 31 syl2anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) e. E )
33 elpwi 
 |-  ( S e. ~P B -> S C_ B )
34 33 sseld 
 |-  ( S e. ~P B -> ( z e. S -> z e. B ) )
35 28 34 syl5com 
 |-  ( z e. ( S \ { X } ) -> ( S e. ~P B -> z e. B ) )
36 35 3ad2ant3 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> ( S e. ~P B -> z e. B ) )
37 36 com12 
 |-  ( S e. ~P B -> ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> z e. B ) )
38 37 3ad2ant1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> z e. B ) )
39 38 imp 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> z e. B )
40 eqid 
 |-  ( .s ` M ) = ( .s ` M )
41 1 2 40 3 9 lmodvsass 
 |-  ( ( M e. LMod /\ ( ( N ` ( F ` X ) ) e. E /\ ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) e. E /\ z e. B ) ) -> ( ( ( N ` ( F ` X ) ) .x. ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ) ( .s ` M ) z ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ( .s ` M ) z ) ) )
42 41 eqcomd 
 |-  ( ( M e. LMod /\ ( ( N ` ( F ` X ) ) e. E /\ ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) e. E /\ z e. B ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ( .s ` M ) z ) ) = ( ( ( N ` ( F ` X ) ) .x. ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ) ( .s ` M ) z ) )
43 19 25 32 39 42 syl13anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ( .s ` M ) z ) ) = ( ( ( N ` ( F ` X ) ) .x. ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ) ( .s ` M ) z ) )
44 2 lmodring 
 |-  ( M e. LMod -> R e. Ring )
45 44 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> R e. Ring )
46 45 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> R e. Ring )
47 elmapi 
 |-  ( F e. ( E ^m S ) -> F : S --> E )
48 ffvelrn 
 |-  ( ( F : S --> E /\ z e. S ) -> ( F ` z ) e. E )
49 47 28 48 syl2an 
 |-  ( ( F e. ( E ^m S ) /\ z e. ( S \ { X } ) ) -> ( F ` z ) e. E )
50 49 3adant2 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> ( F ` z ) e. E )
51 50 adantl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( F ` z ) e. E )
52 simp2 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) -> ( F ` X ) e. U )
53 52 adantl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( F ` X ) e. U )
54 3 4 7 8 9 invginvrid 
 |-  ( ( R e. Ring /\ ( F ` z ) e. E /\ ( F ` X ) e. U ) -> ( ( N ` ( F ` X ) ) .x. ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ) = ( F ` z ) )
55 46 51 53 54 syl3anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( N ` ( F ` X ) ) .x. ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ) = ( F ` z ) )
56 55 oveq1d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( ( N ` ( F ` X ) ) .x. ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` z ) ) ) ( .s ` M ) z ) = ( ( F ` z ) ( .s ` M ) z ) )
57 17 43 56 3eqtrd 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) = ( ( F ` z ) ( .s ` M ) z ) )