Theorem scmatsubcl

Description: The difference of two scalar matrices is a scalar matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatid.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
	scmatid.0	⊢ 0 = ( 0g ‘ 𝑅 )
	scmatid.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion	scmatsubcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		scmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		scmatid.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
4		scmatid.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		scmatid.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
6		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
7		eqid	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
8	3 1 2 6 7 5	scmatscmid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑆 ) → ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
9	8	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑋 ∈ 𝑆 ) → ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
10	9	adantrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
11	3 1 2 6 7 5	scmatscmid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑆 ) → ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
12	11	3expia	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝑆 → ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
13		oveq12	⊢ ( ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) = ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
14	13	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) ∧ ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) = ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
15		eqid	⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
16		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
17		eqid	⊢ ( -g ‘ 𝐴 ) = ( -g ‘ 𝐴 )
18		eqid	⊢ ( -g ‘ ( Scalar ‘ 𝐴 ) ) = ( -g ‘ ( Scalar ‘ 𝐴 ) )
19	1	matlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
20	19	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → 𝐴 ∈ LMod )
21	1	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
22	21	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
23	3 22	eqtrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐸 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
24	23	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑐 ∈ 𝐸 ↔ 𝑐 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
25	24	biimpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑐 ∈ 𝐸 → 𝑐 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
26	25	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ∈ 𝐸 → 𝑐 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
27	26	imp	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → 𝑐 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
28	23	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑑 ∈ 𝐸 ↔ 𝑑 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
29	28	biimpa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) → 𝑑 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
30	29	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → 𝑑 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
31	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
32	2 6	ringidcl	⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
33	31 32	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
34	33	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
35	2 7 15 16 17 18 20 27 30 34	lmodsubdir	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
36	35	eqcomd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) = ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
37		simpll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
38	21	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝐴 ) = 𝑅 )
39	38	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( Scalar ‘ 𝐴 ) = 𝑅 )
40	39	fveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( -g ‘ ( Scalar ‘ 𝐴 ) ) = ( -g ‘ 𝑅 ) )
41	40	oveqd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) = ( 𝑐 ( -g ‘ 𝑅 ) 𝑑 ) )
42		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
43	42	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Grp )
44	43	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → 𝑅 ∈ Grp )
45		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → 𝑐 ∈ 𝐸 )
46		simplr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → 𝑑 ∈ 𝐸 )
47		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
48	3 47	grpsubcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ( -g ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 )
49	44 45 46 48	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑐 ( -g ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 )
50	41 49	eqeltrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ∈ 𝐸 )
51	3 1 2 7	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ∈ 𝐸 ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) ) → ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
52	37 50 34 51	syl12anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
53		oveq1	⊢ ( 𝑒 = ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) → ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
54	53	eqeq2d	⊢ ( 𝑒 = ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) → ( ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
55	54	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑒 = ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ) → ( ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
56		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
57	50 55 56	rspcedvd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
58	3 1 2 6 7 5	scmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
59	58	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
60	52 57 59	mpbir2and	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( -g ‘ ( Scalar ‘ 𝐴 ) ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 )
61	36 60	eqeltrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
62	61	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) ∧ ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
63	14 62	eqeltrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) ∧ ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )
64	63	exp32	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
65	64	rexlimdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
66	65	com23	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑑 ∈ 𝐸 ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
67	66	rexlimdva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
68	12 67	syldc	⊢ ( 𝑌 ∈ 𝑆 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
69	68	adantl	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
70	69	impcom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) )
71	10 70	mpd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 ( -g ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )