Metamath Proof Explorer

Theorem scmataddcl

Description: The sum of two scalar matrices is a scalar matrix. (Contributed by AV, 25-Dec-2019)

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