Metamath Proof Explorer

Theorem lincresunit3lem3

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

Ref Expression
Hypotheses lincresunit3lem3.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lincresunit3lem3.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
lincresunit3lem3.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
lincresunit3lem3.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
lincresunit3lem3.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
lincresunit3lem3.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
Assertion lincresunit3lem3 ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lincresunit3lem3.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lincresunit3lem3.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3 lincresunit3lem3.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
4 lincresunit3lem3.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
5 lincresunit3lem3.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
6 lincresunit3lem3.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
7 3simpa ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) )
8 7 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 1 2 6 9 lmodvs1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
11 8 10 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
12 2 lmodring ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Ring )
13 12 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
14 13 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → 𝑅 ∈ Ring )
15 4 5 unitnegcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑈 )
16 12 15 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑈 )
17 16 3ad2antl1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑈 )
18 14 17 jca ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑈 ) )
19 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
20 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21 4 19 20 9 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
22 18 21 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
23 22 eqcomd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 1r ‘ 𝑅 ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) )
24 23 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑋 ) )
25 11 24 eqtr3d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → 𝑋 = ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑋 ) )
26 25 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → 𝑋 = ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑋 ) )
27 simpl1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → 𝑀 ∈ LMod )
28 4 19 3 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 )
29 18 28 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 )
30 2 lmodfgrp ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Grp )
31 30 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Grp )
32 3 4 unitcl ⊢ ( 𝐴 ∈ 𝑈 → 𝐴 ∈ 𝐸 )
33 3 5 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝐸 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 )
34 31 32 33 syl2an ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 )
35 simpl2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
36 29 34 35 3jca ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑋 ∈ 𝐵 ) )
37 27 36 jca ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑀 ∈ LMod ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑋 ∈ 𝐵 ) ) )
38 37 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( 𝑀 ∈ LMod ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑋 ∈ 𝐵 ) ) )
39 1 2 6 3 20 lmodvsass ⊢ ( ( 𝑀 ∈ LMod ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) ) )
40 38 39 syl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) ) )
41 oveq2 ⊢ ( ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
42 41 adantl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
43 27 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → 𝑀 ∈ LMod )
44 simpl3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → 𝑌 ∈ 𝐵 )
45 29 34 44 3jca ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) )
46 45 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) )
47 43 46 jca ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( 𝑀 ∈ LMod ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) ) )
48 1 2 6 3 20 lmodvsass ⊢ ( ( 𝑀 ∈ LMod ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
49 47 48 syl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
50 18 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑈 ) )
51 50 21 syl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
52 51 oveq1d ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑌 ) = ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
53 49 52 eqtr3d ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) · ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
54 40 42 53 3eqtrd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝑁 ‘ 𝐴 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
55 3simpb ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) )
56 55 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) )
57 56 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) )
58 1 2 6 9 lmodvs1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
59 57 58 syl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
60 26 54 59 3eqtrd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) ∧ ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) → 𝑋 = 𝑌 )
61 60 ex ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) → 𝑋 = 𝑌 ) )
62 oveq2 ⊢ ( 𝑋 = 𝑌 → ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) )
63 61 62 impbid1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ↔ 𝑋 = 𝑌 ) )