Metamath Proof Explorer

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 syl5eq ⊢ ( ( 𝑁 ∈ 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 ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )