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 ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )