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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( ( ( 𝑁 ‘ 𝐴 ) · 𝑋 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ↔ 𝑋 = 𝑌 ) )