Metamath Proof Explorer

Theorem mat1dimmul

Description: The ring multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019) (Proof shortened by AV, 18-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2 mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4 snfi ⊢ { 𝐸 } ∈ Fin
5 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
6 eqid ⊢ ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ ) = ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ )
7 1 6 matmulr ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ ) = ( .r ‘ 𝐴 ) )
8 7 eqcomd ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( .r ‘ 𝐴 ) = ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ ) )
9 4 5 8 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( .r ‘ 𝐴 ) = ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ ) )
10 9 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( .r ‘ 𝐴 ) = ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ ) )
11 10 oveqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = ( { ⟨ 𝑂 , 𝑋 ⟩ } ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ ) { ⟨ 𝑂 , 𝑌 ⟩ } ) )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 5 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
14 4 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { 𝐸 } ∈ Fin )
15 opex ⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
16 15 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ⟨ 𝐸 , 𝐸 ⟩ ∈ V )
17 simpl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
18 17 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
19 16 18 fsnd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 )
20 3 opeq1i ⊢ ⟨ 𝑂 , 𝑋 ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩
21 20 sneqi ⊢ { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ }
22 21 a1i ⊢ ( 𝐸 ∈ 𝑉 → { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } )
23 xpsng ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
24 23 anidms ⊢ ( 𝐸 ∈ 𝑉 → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
25 22 24 feq12d ⊢ ( 𝐸 ∈ 𝑉 → ( { ⟨ 𝑂 , 𝑋 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ) )
26 25 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ) )
27 19 26 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , 𝑋 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 )
28 2 fvexi ⊢ 𝐵 ∈ V
29 28 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 ∈ V )
30 snex ⊢ { 𝐸 } ∈ V
31 30 30 xpex ⊢ ( { 𝐸 } × { 𝐸 } ) ∈ V
32 31 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { 𝐸 } × { 𝐸 } ) ∈ V )
33 29 32 elmapd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ↔ { ⟨ 𝑂 , 𝑋 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
34 27 33 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) )
35 simpr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
36 35 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
37 16 36 fsnd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 )
38 3 opeq1i ⊢ ⟨ 𝑂 , 𝑌 ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩
39 38 sneqi ⊢ { ⟨ 𝑂 , 𝑌 ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ }
40 39 a1i ⊢ ( 𝐸 ∈ 𝑉 → { ⟨ 𝑂 , 𝑌 ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } )
41 40 24 feq12d ⊢ ( 𝐸 ∈ 𝑉 → ( { ⟨ 𝑂 , 𝑌 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ) )
42 41 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ) )
43 37 42 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , 𝑌 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 )
44 29 32 elmapd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑌 ⟩ } ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ↔ { ⟨ 𝑂 , 𝑌 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
45 43 44 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , 𝑌 ⟩ } ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) )
46 6 2 12 13 14 14 14 34 45 mamuval ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ( 𝑅 maMul ⟨ { 𝐸 } , { 𝐸 } , { 𝐸 } ⟩ ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) ) )
47 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐸 ∈ 𝑉 )
48 47 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐸 ∈ 𝑉 )
49 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
50 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
51 50 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑅 ∈ CMnd )
52 df-ov ⊢ ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) = ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ )
53 21 fveq1i ⊢ ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ )
54 52 53 eqtri ⊢ ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) = ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ )
55 15 a1i ⊢ ( 𝑌 ∈ 𝐵 → ⟨ 𝐸 , 𝐸 ⟩ ∈ V )
56 55 anim2i ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ ⟨ 𝐸 , 𝐸 ⟩ ∈ V ) )
57 56 ancomd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⟨ 𝐸 , 𝐸 ⟩ ∈ V ∧ 𝑋 ∈ 𝐵 ) )
58 fvsng ⊢ ( ( ⟨ 𝐸 , 𝐸 ⟩ ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑋 )
59 57 58 syl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑋 )
60 59 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑋 )
61 54 60 eqtrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) = 𝑋 )
62 61 18 eqeltrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ∈ 𝐵 )
63 df-ov ⊢ ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) = ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ )
64 39 fveq1i ⊢ ( { ⟨ 𝑂 , 𝑌 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ )
65 63 64 eqtri ⊢ ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) = ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ )
66 15 a1i ⊢ ( 𝑋 ∈ 𝐵 → ⟨ 𝐸 , 𝐸 ⟩ ∈ V )
67 fvsng ⊢ ( ( ⟨ 𝐸 , 𝐸 ⟩ ∈ V ∧ 𝑌 ∈ 𝐵 ) → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑌 )
68 66 67 sylan ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑌 )
69 68 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑌 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑌 )
70 65 69 eqtrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) = 𝑌 )
71 70 36 eqeltrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ∈ 𝐵 )
72 2 12 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ∈ 𝐵 ∧ ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ∈ 𝐵 ) → ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ 𝐵 )
73 13 62 71 72 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ 𝐵 )
74 oveq2 ⊢ ( 𝑘 = 𝐸 → ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) = ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) )
75 oveq1 ⊢ ( 𝑘 = 𝐸 → ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) = ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) )
76 74 75 oveq12d ⊢ ( 𝑘 = 𝐸 → ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) = ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) )
77 2 eqcomi ⊢ ( Base ‘ 𝑅 ) = 𝐵
78 77 a1i ⊢ ( 𝑘 = 𝐸 → ( Base ‘ 𝑅 ) = 𝐵 )
79 76 78 eleq12d ⊢ ( 𝑘 = 𝐸 → ( ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ 𝐵 ) )
80 79 ralsng ⊢ ( 𝐸 ∈ 𝑉 → ( ∀ 𝑘 ∈ { 𝐸 } ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ 𝐵 ) )
81 80 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∀ 𝑘 ∈ { 𝐸 } ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ 𝐵 ) )
82 73 81 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ∀ 𝑘 ∈ { 𝐸 } ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ ( Base ‘ 𝑅 ) )
83 49 51 14 82 gsummptcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
84 eqid ⊢ ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) )
85 oveq1 ⊢ ( 𝑥 = 𝐸 → ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) = ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) )
86 85 oveq1d ⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) = ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) )
87 86 mpteq2dv ⊢ ( 𝑥 = 𝐸 → ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) = ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) )
88 87 oveq2d ⊢ ( 𝑥 = 𝐸 → ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) )
89 oveq2 ⊢ ( 𝑦 = 𝐸 → ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) = ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) )
90 89 oveq2d ⊢ ( 𝑦 = 𝐸 → ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) = ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) )
91 90 mpteq2dv ⊢ ( 𝑦 = 𝐸 → ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) = ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) )
92 91 oveq2d ⊢ ( 𝑦 = 𝐸 → ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) )
93 84 88 92 mposn ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) ) = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) ⟩ } )
94 48 48 83 93 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) ) = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) ⟩ } )
95 3 eqcomi ⊢ ⟨ 𝐸 , 𝐸 ⟩ = 𝑂
96 95 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ⟨ 𝐸 , 𝐸 ⟩ = 𝑂 )
97 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
98 97 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑅 ∈ Mnd )
99 2 76 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐸 ∈ 𝑉 ∧ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ∈ 𝐵 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) = ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) )
100 98 48 73 99 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) = ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) )
101 96 100 opeq12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) ⟩ = ⟨ 𝑂 , ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ⟩ )
102 101 sneqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ) ) ⟩ } = { ⟨ 𝑂 , ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ⟩ } )
103 61 70 oveq12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) = ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) )
104 103 opeq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ⟨ 𝑂 , ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ⟩ = ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ )
105 104 sneqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → { ⟨ 𝑂 , ( ( 𝐸 { ⟨ 𝑂 , 𝑋 ⟩ } 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 { ⟨ 𝑂 , 𝑌 ⟩ } 𝐸 ) ) ⟩ } = { ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ } )
106 94 102 105 3eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝐸 } ↦ ( ( 𝑥 { ⟨ 𝑂 , 𝑋 ⟩ } 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 { ⟨ 𝑂 , 𝑌 ⟩ } 𝑦 ) ) ) ) ) = { ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ } )
107 11 46 106 3eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑌 ⟩ } ) = { ⟨ 𝑂 , ( 𝑋 ( .r ‘ 𝑅 ) 𝑌 ) ⟩ } )