Step | Hyp | Ref
| Expression |
1 | | snfi 8038 |
. . . . 5
⊢ {𝐸} ∈ Fin |
2 | | simpl 473 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Ring) |
3 | | mat1dim.a |
. . . . . . 7
⊢ 𝐴 = ({𝐸} Mat 𝑅) |
4 | | eqid 2622 |
. . . . . . 7
⊢ (𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉) = (𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉) |
5 | 3, 4 | matmulr 20244 |
. . . . . 6
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉) = (.r‘𝐴)) |
6 | 5 | eqcomd 2628 |
. . . . 5
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) →
(.r‘𝐴) =
(𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉)) |
7 | 1, 2, 6 | sylancr 695 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (.r‘𝐴) = (𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉)) |
8 | 7 | adantr 481 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (.r‘𝐴) = (𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉)) |
9 | 8 | oveqd 6667 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈𝑂, 𝑋〉} (.r‘𝐴){〈𝑂, 𝑌〉}) = ({〈𝑂, 𝑋〉} (𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉){〈𝑂, 𝑌〉})) |
10 | | mat1dim.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
11 | | eqid 2622 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
12 | 2 | adantr 481 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑅 ∈ Ring) |
13 | 1 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {𝐸} ∈ Fin) |
14 | | opex 4932 |
. . . . . . 7
⊢
〈𝐸, 𝐸〉 ∈ V |
15 | 14 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 〈𝐸, 𝐸〉 ∈ V) |
16 | | simpl 473 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
17 | 16 | adantl 482 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
18 | 15, 17 | fsnd 6179 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈〈𝐸, 𝐸〉, 𝑋〉}:{〈𝐸, 𝐸〉}⟶𝐵) |
19 | | mat1dim.o |
. . . . . . . . . 10
⊢ 𝑂 = 〈𝐸, 𝐸〉 |
20 | 19 | opeq1i 4405 |
. . . . . . . . 9
⊢
〈𝑂, 𝑋〉 = 〈〈𝐸, 𝐸〉, 𝑋〉 |
21 | 20 | sneqi 4188 |
. . . . . . . 8
⊢
{〈𝑂, 𝑋〉} = {〈〈𝐸, 𝐸〉, 𝑋〉} |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝐸 ∈ 𝑉 → {〈𝑂, 𝑋〉} = {〈〈𝐸, 𝐸〉, 𝑋〉}) |
23 | | xpsng 6406 |
. . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) |
24 | 23 | anidms 677 |
. . . . . . 7
⊢ (𝐸 ∈ 𝑉 → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) |
25 | 22, 24 | feq12d 6033 |
. . . . . 6
⊢ (𝐸 ∈ 𝑉 → ({〈𝑂, 𝑋〉}:({𝐸} × {𝐸})⟶𝐵 ↔ {〈〈𝐸, 𝐸〉, 𝑋〉}:{〈𝐸, 𝐸〉}⟶𝐵)) |
26 | 25 | ad2antlr 763 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈𝑂, 𝑋〉}:({𝐸} × {𝐸})⟶𝐵 ↔ {〈〈𝐸, 𝐸〉, 𝑋〉}:{〈𝐸, 𝐸〉}⟶𝐵)) |
27 | 18, 26 | mpbird 247 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈𝑂, 𝑋〉}:({𝐸} × {𝐸})⟶𝐵) |
28 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
29 | 10, 28 | eqeltri 2697 |
. . . . . 6
⊢ 𝐵 ∈ V |
30 | 29 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 ∈ V) |
31 | | snex 4908 |
. . . . . . 7
⊢ {𝐸} ∈ V |
32 | 31, 31 | xpex 6962 |
. . . . . 6
⊢ ({𝐸} × {𝐸}) ∈ V |
33 | 32 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({𝐸} × {𝐸}) ∈ V) |
34 | 30, 33 | elmapd 7871 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈𝑂, 𝑋〉} ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸})) ↔ {〈𝑂, 𝑋〉}:({𝐸} × {𝐸})⟶𝐵)) |
35 | 27, 34 | mpbird 247 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈𝑂, 𝑋〉} ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸}))) |
36 | | simpr 477 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
37 | 36 | adantl 482 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
38 | 15, 37 | fsnd 6179 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈〈𝐸, 𝐸〉, 𝑌〉}:{〈𝐸, 𝐸〉}⟶𝐵) |
39 | 19 | opeq1i 4405 |
. . . . . . . . 9
⊢
〈𝑂, 𝑌〉 = 〈〈𝐸, 𝐸〉, 𝑌〉 |
40 | 39 | sneqi 4188 |
. . . . . . . 8
⊢
{〈𝑂, 𝑌〉} = {〈〈𝐸, 𝐸〉, 𝑌〉} |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝐸 ∈ 𝑉 → {〈𝑂, 𝑌〉} = {〈〈𝐸, 𝐸〉, 𝑌〉}) |
42 | 41, 24 | feq12d 6033 |
. . . . . 6
⊢ (𝐸 ∈ 𝑉 → ({〈𝑂, 𝑌〉}:({𝐸} × {𝐸})⟶𝐵 ↔ {〈〈𝐸, 𝐸〉, 𝑌〉}:{〈𝐸, 𝐸〉}⟶𝐵)) |
43 | 42 | ad2antlr 763 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈𝑂, 𝑌〉}:({𝐸} × {𝐸})⟶𝐵 ↔ {〈〈𝐸, 𝐸〉, 𝑌〉}:{〈𝐸, 𝐸〉}⟶𝐵)) |
44 | 38, 43 | mpbird 247 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈𝑂, 𝑌〉}:({𝐸} × {𝐸})⟶𝐵) |
45 | 30, 33 | elmapd 7871 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈𝑂, 𝑌〉} ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸})) ↔ {〈𝑂, 𝑌〉}:({𝐸} × {𝐸})⟶𝐵)) |
46 | 44, 45 | mpbird 247 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈𝑂, 𝑌〉} ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸}))) |
47 | 4, 10, 11, 12, 13, 13, 13, 35, 46 | mamuval 20192 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈𝑂, 𝑋〉} (𝑅 maMul 〈{𝐸}, {𝐸}, {𝐸}〉){〈𝑂, 𝑌〉}) = (𝑥 ∈ {𝐸}, 𝑦 ∈ {𝐸} ↦ (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦)))))) |
48 | | simpr 477 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐸 ∈ 𝑉) |
49 | 48 | adantr 481 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐸 ∈ 𝑉) |
50 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
51 | | ringcmn 18581 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
52 | 51 | ad2antrr 762 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑅 ∈ CMnd) |
53 | | df-ov 6653 |
. . . . . . . . . 10
⊢ (𝐸{〈𝑂, 𝑋〉}𝐸) = ({〈𝑂, 𝑋〉}‘〈𝐸, 𝐸〉) |
54 | 21 | fveq1i 6192 |
. . . . . . . . . 10
⊢
({〈𝑂, 𝑋〉}‘〈𝐸, 𝐸〉) = ({〈〈𝐸, 𝐸〉, 𝑋〉}‘〈𝐸, 𝐸〉) |
55 | 53, 54 | eqtri 2644 |
. . . . . . . . 9
⊢ (𝐸{〈𝑂, 𝑋〉}𝐸) = ({〈〈𝐸, 𝐸〉, 𝑋〉}‘〈𝐸, 𝐸〉) |
56 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝐵 → 〈𝐸, 𝐸〉 ∈ V) |
57 | 56 | anim2i 593 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∈ 𝐵 ∧ 〈𝐸, 𝐸〉 ∈ V)) |
58 | 57 | ancomd 467 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝐸, 𝐸〉 ∈ V ∧ 𝑋 ∈ 𝐵)) |
59 | | fvsng 6447 |
. . . . . . . . . . 11
⊢
((〈𝐸, 𝐸〉 ∈ V ∧ 𝑋 ∈ 𝐵) → ({〈〈𝐸, 𝐸〉, 𝑋〉}‘〈𝐸, 𝐸〉) = 𝑋) |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({〈〈𝐸, 𝐸〉, 𝑋〉}‘〈𝐸, 𝐸〉) = 𝑋) |
61 | 60 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈〈𝐸, 𝐸〉, 𝑋〉}‘〈𝐸, 𝐸〉) = 𝑋) |
62 | 55, 61 | syl5eq 2668 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐸{〈𝑂, 𝑋〉}𝐸) = 𝑋) |
63 | 62, 17 | eqeltrd 2701 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐸{〈𝑂, 𝑋〉}𝐸) ∈ 𝐵) |
64 | | df-ov 6653 |
. . . . . . . . . 10
⊢ (𝐸{〈𝑂, 𝑌〉}𝐸) = ({〈𝑂, 𝑌〉}‘〈𝐸, 𝐸〉) |
65 | 40 | fveq1i 6192 |
. . . . . . . . . 10
⊢
({〈𝑂, 𝑌〉}‘〈𝐸, 𝐸〉) = ({〈〈𝐸, 𝐸〉, 𝑌〉}‘〈𝐸, 𝐸〉) |
66 | 64, 65 | eqtri 2644 |
. . . . . . . . 9
⊢ (𝐸{〈𝑂, 𝑌〉}𝐸) = ({〈〈𝐸, 𝐸〉, 𝑌〉}‘〈𝐸, 𝐸〉) |
67 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐵 → 〈𝐸, 𝐸〉 ∈ V) |
68 | | fvsng 6447 |
. . . . . . . . . . 11
⊢
((〈𝐸, 𝐸〉 ∈ V ∧ 𝑌 ∈ 𝐵) → ({〈〈𝐸, 𝐸〉, 𝑌〉}‘〈𝐸, 𝐸〉) = 𝑌) |
69 | 67, 68 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({〈〈𝐸, 𝐸〉, 𝑌〉}‘〈𝐸, 𝐸〉) = 𝑌) |
70 | 69 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈〈𝐸, 𝐸〉, 𝑌〉}‘〈𝐸, 𝐸〉) = 𝑌) |
71 | 66, 70 | syl5eq 2668 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐸{〈𝑂, 𝑌〉}𝐸) = 𝑌) |
72 | 71, 37 | eqeltrd 2701 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐸{〈𝑂, 𝑌〉}𝐸) ∈ 𝐵) |
73 | 10, 11 | ringcl 18561 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐸{〈𝑂, 𝑋〉}𝐸) ∈ 𝐵 ∧ (𝐸{〈𝑂, 𝑌〉}𝐸) ∈ 𝐵) → ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸)) ∈ 𝐵) |
74 | 12, 63, 72, 73 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸)) ∈ 𝐵) |
75 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐸 → (𝐸{〈𝑂, 𝑋〉}𝑘) = (𝐸{〈𝑂, 𝑋〉}𝐸)) |
76 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐸 → (𝑘{〈𝑂, 𝑌〉}𝐸) = (𝐸{〈𝑂, 𝑌〉}𝐸)) |
77 | 75, 76 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑘 = 𝐸 → ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)) = ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸))) |
78 | 10 | eqcomi 2631 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
𝐵 |
79 | 78 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 = 𝐸 → (Base‘𝑅) = 𝐵) |
80 | 77, 79 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑘 = 𝐸 → (((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)) ∈ (Base‘𝑅) ↔ ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸)) ∈ 𝐵)) |
81 | 80 | ralsng 4218 |
. . . . . . 7
⊢ (𝐸 ∈ 𝑉 → (∀𝑘 ∈ {𝐸} ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)) ∈ (Base‘𝑅) ↔ ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸)) ∈ 𝐵)) |
82 | 81 | ad2antlr 763 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (∀𝑘 ∈ {𝐸} ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)) ∈ (Base‘𝑅) ↔ ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸)) ∈ 𝐵)) |
83 | 74, 82 | mpbird 247 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ∀𝑘 ∈ {𝐸} ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)) ∈ (Base‘𝑅)) |
84 | 50, 52, 13, 83 | gsummptcl 18366 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)))) ∈ (Base‘𝑅)) |
85 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ {𝐸}, 𝑦 ∈ {𝐸} ↦ (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))))) = (𝑥 ∈ {𝐸}, 𝑦 ∈ {𝐸} ↦ (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))))) |
86 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 𝐸 → (𝑥{〈𝑂, 𝑋〉}𝑘) = (𝐸{〈𝑂, 𝑋〉}𝑘)) |
87 | 86 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 𝐸 → ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦)) = ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))) |
88 | 87 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝑥 = 𝐸 → (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))) = (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦)))) |
89 | 88 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝐸 → (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦)))) = (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))))) |
90 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = 𝐸 → (𝑘{〈𝑂, 𝑌〉}𝑦) = (𝑘{〈𝑂, 𝑌〉}𝐸)) |
91 | 90 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑦 = 𝐸 → ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦)) = ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸))) |
92 | 91 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝑦 = 𝐸 → (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))) = (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)))) |
93 | 92 | oveq2d 6666 |
. . . . 5
⊢ (𝑦 = 𝐸 → (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦)))) = (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸))))) |
94 | 85, 89, 93 | mpt2sn 7268 |
. . . 4
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)))) ∈ (Base‘𝑅)) → (𝑥 ∈ {𝐸}, 𝑦 ∈ {𝐸} ↦ (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))))) = {〈〈𝐸, 𝐸〉, (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸))))〉}) |
95 | 49, 49, 84, 94 | syl3anc 1326 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑥 ∈ {𝐸}, 𝑦 ∈ {𝐸} ↦ (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))))) = {〈〈𝐸, 𝐸〉, (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸))))〉}) |
96 | 19 | eqcomi 2631 |
. . . . . 6
⊢
〈𝐸, 𝐸〉 = 𝑂 |
97 | 96 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 〈𝐸, 𝐸〉 = 𝑂) |
98 | | ringmnd 18556 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
99 | 98 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑅 ∈ Mnd) |
100 | 10, 77 | gsumsn 18354 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ 𝐸 ∈ 𝑉 ∧ ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸)) ∈ 𝐵) → (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)))) = ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸))) |
101 | 99, 49, 74, 100 | syl3anc 1326 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸)))) = ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸))) |
102 | 97, 101 | opeq12d 4410 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 〈〈𝐸, 𝐸〉, (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸))))〉 = 〈𝑂, ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸))〉) |
103 | 102 | sneqd 4189 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈〈𝐸, 𝐸〉, (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝐸{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝐸))))〉} = {〈𝑂, ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸))〉}) |
104 | 62, 71 | oveq12d 6668 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸)) = (𝑋(.r‘𝑅)𝑌)) |
105 | 104 | opeq2d 4409 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 〈𝑂, ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸))〉 = 〈𝑂, (𝑋(.r‘𝑅)𝑌)〉) |
106 | 105 | sneqd 4189 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → {〈𝑂, ((𝐸{〈𝑂, 𝑋〉}𝐸)(.r‘𝑅)(𝐸{〈𝑂, 𝑌〉}𝐸))〉} = {〈𝑂, (𝑋(.r‘𝑅)𝑌)〉}) |
107 | 95, 103, 106 | 3eqtrd 2660 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑥 ∈ {𝐸}, 𝑦 ∈ {𝐸} ↦ (𝑅 Σg (𝑘 ∈ {𝐸} ↦ ((𝑥{〈𝑂, 𝑋〉}𝑘)(.r‘𝑅)(𝑘{〈𝑂, 𝑌〉}𝑦))))) = {〈𝑂, (𝑋(.r‘𝑅)𝑌)〉}) |
108 | 9, 47, 107 | 3eqtrd 2660 |
1
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({〈𝑂, 𝑋〉} (.r‘𝐴){〈𝑂, 𝑌〉}) = {〈𝑂, (𝑋(.r‘𝑅)𝑌)〉}) |