This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) 𝑌 ) ⟩ } )