Metamath Proof Explorer

Theorem lincresunit3lem3

Description: Lemma 3 for lincresunit3 . (Contributed by AV, 18-May-2019)

Ref Expression
Hypotheses lincresunit3lem3.b 
|- B = ( Base ` M )
lincresunit3lem3.r 
|- R = ( Scalar ` M )
lincresunit3lem3.e 
|- E = ( Base ` R )
lincresunit3lem3.u 
|- U = ( Unit ` R )
lincresunit3lem3.n 
|- N = ( invg ` R )
lincresunit3lem3.t 
|- .x. = ( .s ` M )
Assertion lincresunit3lem3 
|- ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 lincresunit3lem3.b 
 |-  B = ( Base ` M )
2 lincresunit3lem3.r 
 |-  R = ( Scalar ` M )
3 lincresunit3lem3.e 
 |-  E = ( Base ` R )
4 lincresunit3lem3.u 
 |-  U = ( Unit ` R )
5 lincresunit3lem3.n 
 |-  N = ( invg ` R )
6 lincresunit3lem3.t 
 |-  .x. = ( .s ` M )
7 3simpa 
 |-  ( ( M e. LMod /\ X e. B /\ Y e. B ) -> ( M e. LMod /\ X e. B ) )
8 7 adantr 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( M e. LMod /\ X e. B ) )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 1 2 6 9 lmodvs1 
 |-  ( ( M e. LMod /\ X e. B ) -> ( ( 1r ` R ) .x. X ) = X )
11 8 10 syl 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( 1r ` R ) .x. X ) = X )
12 2 lmodring 
 |-  ( M e. LMod -> R e. Ring )
13 12 3ad2ant1 
 |-  ( ( M e. LMod /\ X e. B /\ Y e. B ) -> R e. Ring )
14 13 adantr 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> R e. Ring )
15 4 5 unitnegcl 
 |-  ( ( R e. Ring /\ A e. U ) -> ( N ` A ) e. U )
16 12 15 sylan 
 |-  ( ( M e. LMod /\ A e. U ) -> ( N ` A ) e. U )
17 16 3ad2antl1 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( N ` A ) e. U )
18 14 17 jca 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( R e. Ring /\ ( N ` A ) e. U ) )
19 eqid 
 |-  ( invr ` R ) = ( invr ` R )
20 eqid 
 |-  ( .r ` R ) = ( .r ` R )
21 4 19 20 9 unitlinv 
 |-  ( ( R e. Ring /\ ( N ` A ) e. U ) -> ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) = ( 1r ` R ) )
22 18 21 syl 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) = ( 1r ` R ) )
23 22 eqcomd 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( 1r ` R ) = ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) )
24 23 oveq1d 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( 1r ` R ) .x. X ) = ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. X ) )
25 11 24 eqtr3d 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> X = ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. X ) )
26 25 adantr 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> X = ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. X ) )
27 simpl1 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> M e. LMod )
28 4 19 3 ringinvcl 
 |-  ( ( R e. Ring /\ ( N ` A ) e. U ) -> ( ( invr ` R ) ` ( N ` A ) ) e. E )
29 18 28 syl 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( invr ` R ) ` ( N ` A ) ) e. E )
30 2 lmodfgrp 
 |-  ( M e. LMod -> R e. Grp )
31 30 3ad2ant1 
 |-  ( ( M e. LMod /\ X e. B /\ Y e. B ) -> R e. Grp )
32 3 4 unitcl 
 |-  ( A e. U -> A e. E )
33 3 5 grpinvcl 
 |-  ( ( R e. Grp /\ A e. E ) -> ( N ` A ) e. E )
34 31 32 33 syl2an 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( N ` A ) e. E )
35 simpl2 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> X e. B )
36 29 34 35 3jca 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ X e. B ) )
37 27 36 jca 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( M e. LMod /\ ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ X e. B ) ) )
38 37 adantr 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( M e. LMod /\ ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ X e. B ) ) )
39 1 2 6 3 20 lmodvsass 
 |-  ( ( M e. LMod /\ ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ X e. B ) ) -> ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. X ) = ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. X ) ) )
40 38 39 syl 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. X ) = ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. X ) ) )
41 oveq2 
 |-  ( ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) -> ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. X ) ) = ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. Y ) ) )
42 41 adantl 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. X ) ) = ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. Y ) ) )
43 27 adantr 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> M e. LMod )
44 simpl3 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> Y e. B )
45 29 34 44 3jca 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ Y e. B ) )
46 45 adantr 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ Y e. B ) )
47 43 46 jca 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( M e. LMod /\ ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ Y e. B ) ) )
48 1 2 6 3 20 lmodvsass 
 |-  ( ( M e. LMod /\ ( ( ( invr ` R ) ` ( N ` A ) ) e. E /\ ( N ` A ) e. E /\ Y e. B ) ) -> ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. Y ) = ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. Y ) ) )
49 47 48 syl 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. Y ) = ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. Y ) ) )
50 18 adantr 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( R e. Ring /\ ( N ` A ) e. U ) )
51 50 21 syl 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) = ( 1r ` R ) )
52 51 oveq1d 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. Y ) = ( ( 1r ` R ) .x. Y ) )
53 49 52 eqtr3d 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( invr ` R ) ` ( N ` A ) ) .x. ( ( N ` A ) .x. Y ) ) = ( ( 1r ` R ) .x. Y ) )
54 40 42 53 3eqtrd 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( ( ( invr ` R ) ` ( N ` A ) ) ( .r ` R ) ( N ` A ) ) .x. X ) = ( ( 1r ` R ) .x. Y ) )
55 3simpb 
 |-  ( ( M e. LMod /\ X e. B /\ Y e. B ) -> ( M e. LMod /\ Y e. B ) )
56 55 adantr 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( M e. LMod /\ Y e. B ) )
57 56 adantr 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( M e. LMod /\ Y e. B ) )
58 1 2 6 9 lmodvs1 
 |-  ( ( M e. LMod /\ Y e. B ) -> ( ( 1r ` R ) .x. Y ) = Y )
59 57 58 syl 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> ( ( 1r ` R ) .x. Y ) = Y )
60 26 54 59 3eqtrd 
 |-  ( ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) /\ ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) ) -> X = Y )
61 60 ex 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) -> X = Y ) )
62 oveq2 
 |-  ( X = Y -> ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) )
63 61 62 impbid1 
 |-  ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) <-> X = Y ) )