Theorem mat1dimscm

Description: The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019)

	Ref	Expression
Hypotheses	mat1dim.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
	mat1dim.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mat1dim.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion	mat1dimscm	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝐴 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = { ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		mat1dim.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2		mat1dim.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		mat1dim.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4		opex	⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
5	3 4	eqeltri	⊢ 𝑂 ∈ V
6	5	a1i	⊢ ( 𝑌 ∈ 𝐵 → 𝑂 ∈ V )
7	6	anim2i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑂 ∈ V ) )
8	7	ancomd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑂 ∈ V ∧ 𝑋 ∈ 𝐵 ) )
9		fnsng	⊢ ( ( 𝑂 ∈ V ∧ 𝑋 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑋 ⟩ } Fn { 𝑂 } )
10	8 9	syl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑋 ⟩ } Fn { 𝑂 } )
11	10	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , 𝑋 ⟩ } Fn { 𝑂 } )
12		xpsng	⊢ ( ( 𝑂 ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( { 𝑂 } × { 𝑋 } ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
13	8 12	syl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { 𝑂 } × { 𝑋 } ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
14	13	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { 𝑂 } × { 𝑋 } ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
15	14	fneq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( { 𝑂 } × { 𝑋 } ) Fn { 𝑂 } ↔ { ⟨ 𝑂 , 𝑋 ⟩ } Fn { 𝑂 } ) )
16	11 15	mpbird	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { 𝑂 } × { 𝑋 } ) Fn { 𝑂 } )
17		xpsng	⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
18	3	sneqi	⊢ { 𝑂 } = { ⟨ 𝐸 , 𝐸 ⟩ }
19	17 18	eqtr4di	⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { 𝑂 } )
20	19	anidms	⊢ ( 𝐸 ∈ 𝑉 → ( { 𝐸 } × { 𝐸 } ) = { 𝑂 } )
21	20	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { 𝐸 } × { 𝐸 } ) = { 𝑂 } )
22	21	xpeq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) = ( { 𝑂 } × { 𝑋 } ) )
23	22	fneq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) Fn { 𝑂 } ↔ ( { 𝑂 } × { 𝑋 } ) Fn { 𝑂 } ) )
24	16 23	mpbird	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) Fn { 𝑂 } )
25	5	a1i	⊢ ( 𝑋 ∈ 𝐵 → 𝑂 ∈ V )
26		fnsng	⊢ ( ( 𝑂 ∈ V ∧ 𝑌 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑌 ⟩ } Fn { 𝑂 } )
27	25 26	sylan	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑌 ⟩ } Fn { 𝑂 } )
28	27	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , 𝑌 ⟩ } Fn { 𝑂 } )
29		snex	⊢ { 𝑂 } ∈ V
30	29	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { 𝑂 } ∈ V )
31		inidm	⊢ ( { 𝑂 } ∩ { 𝑂 } ) = { 𝑂 }
32		elsni	⊢ ( 𝑥 ∈ { 𝑂 } → 𝑥 = 𝑂 )
33		fveq2	⊢ ( 𝑥 = 𝑂 → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑥 ) = ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑂 ) )
34	17	anidms	⊢ ( 𝐸 ∈ 𝑉 → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
35	34	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
36	35	xpeq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) = ( { ⟨ 𝐸 , 𝐸 ⟩ } × { 𝑋 } ) )
37	4	a1i	⊢ ( 𝑌 ∈ 𝐵 → ⟨ 𝐸 , 𝐸 ⟩ ∈ V )
38	37	anim2i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ ⟨ 𝐸 , 𝐸 ⟩ ∈ V ) )
39	38	ancomd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⟨ 𝐸 , 𝐸 ⟩ ∈ V ∧ 𝑋 ∈ 𝐵 ) )
40		xpsng	⊢ ( ( ⟨ 𝐸 , 𝐸 ⟩ ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝐸 , 𝐸 ⟩ } × { 𝑋 } ) = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } )
41	3	eqcomi	⊢ ⟨ 𝐸 , 𝐸 ⟩ = 𝑂
42	41	opeq1i	⊢ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ = ⟨ 𝑂 , 𝑋 ⟩
43	42	sneqi	⊢ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑋 ⟩ }
44	40 43	eqtrdi	⊢ ( ( ⟨ 𝐸 , 𝐸 ⟩ ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝐸 , 𝐸 ⟩ } × { 𝑋 } ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
45	39 44	syl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { ⟨ 𝐸 , 𝐸 ⟩ } × { 𝑋 } ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
46	45	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝐸 , 𝐸 ⟩ } × { 𝑋 } ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
47	36 46	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
48	47	fveq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑂 ) = ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ 𝑂 ) )
49		fvsng	⊢ ( ( 𝑂 ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ 𝑂 ) = 𝑋 )
50	8 49	syl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ 𝑂 ) = 𝑋 )
51	50	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ 𝑂 ) = 𝑋 )
52	48 51	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑂 ) = 𝑋 )
53	33 52	sylan9eq	⊢ ( ( 𝑥 = 𝑂 ∧ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
54	53	ex	⊢ ( 𝑥 = 𝑂 → ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 ) )
55	32 54	syl	⊢ ( 𝑥 ∈ { 𝑂 } → ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 ) )
56	55	impcom	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑥 ∈ { 𝑂 } ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
57		fveq2	⊢ ( 𝑥 = 𝑂 → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑂 ) )
58		fvsng	⊢ ( ( 𝑂 ∈ V ∧ 𝑌 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑂 ) = 𝑌 )
59	25 58	sylan	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑂 ) = 𝑌 )
60	59	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑂 ) = 𝑌 )
61	57 60	sylan9eq	⊢ ( ( 𝑥 = 𝑂 ∧ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑥 ) = 𝑌 )
62	61	ex	⊢ ( 𝑥 = 𝑂 → ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑥 ) = 𝑌 ) )
63	32 62	syl	⊢ ( 𝑥 ∈ { 𝑂 } → ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑥 ) = 𝑌 ) )
64	63	impcom	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑥 ∈ { 𝑂 } ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ 𝑥 ) = 𝑌 )
65	24 28 30 30 31 56 64	offval	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = ( 𝑥 ∈ { 𝑂 } ↦ ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ) )
66		simprl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
67		simpr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
68	67	anim2i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑌 ∈ 𝐵 ) )
69		df-3an	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑌 ∈ 𝐵 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑌 ∈ 𝐵 ) )
70	68 69	sylibr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑌 ∈ 𝐵 ) )
71	1 2 3	mat1dimbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑌 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑌 ⟩ } ∈ ( Base ‘ 𝐴 ) )
72	70 71	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , 𝑌 ⟩ } ∈ ( Base ‘ 𝐴 ) )
73		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
74		eqid	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
75		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
76		eqid	⊢ ( { 𝐸 } × { 𝐸 } ) = ( { 𝐸 } × { 𝐸 } )
77	1 73 2 74 75 76	matvsca2	⊢ ( ( 𝑋 ∈ 𝐵 ∧ { ⟨ 𝑂 , 𝑌 ⟩ } ∈ ( Base ‘ 𝐴 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝐴 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) )
78	66 72 77	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝐴 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = ( ( ( { 𝐸 } × { 𝐸 } ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) )
79		3anass	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ↔ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) )
80	79	biimpri	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
81	80	adantlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
82	2 75	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ∈ 𝐵 )
83	81 82	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ∈ 𝐵 )
84		fmptsn	⊢ ( ( 𝑂 ∈ V ∧ ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ∈ 𝐵 ) → { ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ } = ( 𝑥 ∈ { 𝑂 } ↦ ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ) )
85	5 83 84	sylancr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ } = ( 𝑥 ∈ { 𝑂 } ↦ ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ) )
86	65 78 85	3eqtr4d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝐴 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = { ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ } )