Theorem scmatmulcl

Description: The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-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	scmatmulcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )

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	scmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
9	3 1 2 6 7 5	scmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
10		oveq12	⊢ ( ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
11	10	adantll	⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
12		simp-4l	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
13		simplr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) → 𝑑 ∈ 𝐸 )
14	13	anim1ci	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) )
15		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16		eqid	⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
17	1 3 4 6 7 15 16	scmatscmiddistr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
18	12 14 17	syl2anc	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
19		simpl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
20		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → 𝑅 ∈ Ring )
21		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → 𝑐 ∈ 𝐸 )
22		simpl	⊢ ( ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) → 𝑑 ∈ 𝐸 )
23	22	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → 𝑑 ∈ 𝐸 )
24	3 15	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 )
25	20 21 23 24	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 )
26	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
27	2 6	ringidcl	⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
28	26 27	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
29	28	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
30	3 1 2 7	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
31	19 25 29 30	syl12anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
32		oveq1	⊢ ( 𝑒 = ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) → ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
33	32	eqeq2d	⊢ ( 𝑒 = ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
34	33	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ 𝑒 = ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
35		eqidd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
36	25 34 35	rspcedvd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
37	3 1 2 6 7 5	scmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
38	37	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
39	31 36 38	mpbir2and	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 )
40	39	exp32	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑑 ∈ 𝐸 → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) ) )
41	40	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝑑 ∈ 𝐸 → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) ) )
42	41	imp	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) )
43	42	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) )
44	43	imp	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 )
45	18 44	eqeltrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
46	45	adantr	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
47	46	adantr	⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
48	11 47	eqeltrd	⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )
49	48	exp31	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
50	49	rexlimdva	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
51	50	expimpd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
52	51	com23	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
53	52	rexlimdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
54	53	expimpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
55	9 54	sylbid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝑆 → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
56	55	com23	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑌 ∈ 𝑆 → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
57	8 56	sylbid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝑆 → ( 𝑌 ∈ 𝑆 → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
58	57	imp32	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )