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