Step | Hyp | Ref
| Expression |
1 | | mdetmul.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | mdetmul.b |
. . 3
⊢ 𝐵 = (Base‘𝐴) |
3 | | eqid 2622 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | | eqid 2622 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | | eqid 2622 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
6 | | eqid 2622 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
7 | | mdetmul.t1 |
. . 3
⊢ · =
(.r‘𝑅) |
8 | 1, 2 | matrcl 20218 |
. . . . 5
⊢ (𝐹 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
9 | 8 | simpld 475 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → 𝑁 ∈ Fin) |
10 | 9 | 3ad2ant2 1083 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑁 ∈ Fin) |
11 | | crngring 18558 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
12 | 11 | 3ad2ant1 1082 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ Ring) |
13 | | mdetmul.d |
. . . . . . . 8
⊢ 𝐷 = (𝑁 maDet 𝑅) |
14 | 13, 1, 2, 3 | mdetf 20401 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅)) |
15 | 14 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅)) |
16 | 15 | adantr 481 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅)) |
17 | 1 | matring 20249 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
18 | 10, 12, 17 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐴 ∈ Ring) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐴 ∈ Ring) |
20 | | simpr 477 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
21 | | simpl3 1066 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
22 | | mdetmul.t2 |
. . . . . . 7
⊢ ∙ =
(.r‘𝐴) |
23 | 2, 22 | ringcl 18561 |
. . . . . 6
⊢ ((𝐴 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵) |
24 | 19, 20, 21, 23 | syl3anc 1326 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵) |
25 | 16, 24 | ffvelrnd 6360 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐷‘(𝑎 ∙ 𝐺)) ∈ (Base‘𝑅)) |
26 | | eqid 2622 |
. . . 4
⊢ (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))) = (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))) |
27 | 25, 26 | fmptd 6385 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))):𝐵⟶(Base‘𝑅)) |
28 | | simp21 1094 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑏 ∈ 𝐵) |
29 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝑎 ∙ 𝐺) = (𝑏 ∙ 𝐺)) |
30 | 29 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑏 ∙ 𝐺))) |
31 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐷‘(𝑏 ∙ 𝐺)) ∈ V |
32 | 30, 26, 31 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺))) |
33 | 28, 32 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺))) |
34 | | simp11 1091 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑅 ∈ CRing) |
35 | 18 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐴 ∈ Ring) |
36 | | simpr1 1067 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝑏 ∈ 𝐵) |
37 | | simpl3 1066 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐺 ∈ 𝐵) |
38 | 2, 22 | ringcl 18561 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑏 ∙ 𝐺) ∈ 𝐵) |
39 | 35, 36, 37, 38 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → (𝑏 ∙ 𝐺) ∈ 𝐵) |
40 | 39 | 3adant3 1081 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝑏 ∙ 𝐺) ∈ 𝐵) |
41 | | simp22 1095 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ∈ 𝑁) |
42 | | simp23 1096 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑑 ∈ 𝑁) |
43 | | simp3l 1089 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ≠ 𝑑) |
44 | | simpl3r 1117 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) |
45 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ 𝑁 = 𝑁 |
46 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ ((𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) |
47 | 46 | ralimi 2952 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) |
48 | | mpteq12 4736 |
. . . . . . . . . . . 12
⊢ ((𝑁 = 𝑁 ∧ ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))) |
49 | 45, 47, 48 | sylancr 695 |
. . . . . . . . . . 11
⊢
(∀𝑒 ∈
𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))) |
50 | 49 | oveq2d 6666 |
. . . . . . . . . 10
⊢
(∀𝑒 ∈
𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))) |
51 | 44, 50 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))) |
52 | | simp1 1061 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ CRing) |
53 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
54 | 1, 53 | matmulr 20244 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
55 | 54, 22 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = ∙ ) |
56 | 10, 52, 55 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = ∙ ) |
57 | 56 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = ∙ ) |
58 | 57 | oveqd 6667 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) = (𝑏 ∙ 𝐺)) |
59 | 58 | oveqd 6667 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺)𝑎) = (𝑐(𝑏 ∙ 𝐺)𝑎)) |
60 | | simpll1 1100 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑅 ∈ CRing) |
61 | 10 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑁 ∈ Fin) |
62 | | simplr1 1103 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ 𝐵) |
63 | 1, 3, 2 | matbas2i 20228 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
65 | 1, 3, 2 | matbas2i 20228 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ 𝐵 → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
66 | 65 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
67 | 66 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
68 | | simplr2 1104 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑐 ∈ 𝑁) |
69 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑎 ∈ 𝑁) |
70 | 53, 3, 7, 60, 61, 61, 61, 64, 67, 68, 69 | mamufv 20193 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))))) |
71 | 59, 70 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))))) |
72 | 71 | 3adantl3 1219 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))))) |
73 | 58 | oveqd 6667 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎)) |
74 | | simplr3 1105 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑑 ∈ 𝑁) |
75 | 53, 3, 7, 60, 61, 61, 61, 64, 67, 74, 69 | mamufv 20193 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))) |
76 | 73, 75 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))) |
77 | 76 | 3adantl3 1219 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))) |
78 | 51, 72, 77 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎)) |
79 | 78 | ralrimiva 2966 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑎 ∈ 𝑁 (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎)) |
80 | 13, 1, 2, 4, 34, 40, 41, 42, 43, 79 | mdetralt 20414 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐷‘(𝑏 ∙ 𝐺)) = (0g‘𝑅)) |
81 | 33, 80 | eqtrd 2656 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0g‘𝑅)) |
82 | 81 | 3expia 1267 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0g‘𝑅))) |
83 | 82 | ralrimivvva 2972 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝑁 ∀𝑑 ∈ 𝑁 ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0g‘𝑅))) |
84 | | simp11 1091 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing) |
85 | 18 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring) |
86 | | simprll 802 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵) |
87 | | simpl3 1066 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵) |
88 | 85, 86, 87, 38 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵) |
89 | 88 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵) |
90 | | simprlr 803 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ 𝐵) |
91 | 2, 22 | ringcl 18561 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Ring ∧ 𝑐 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑐 ∙ 𝐺) ∈ 𝐵) |
92 | 85, 90, 87, 91 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ∙ 𝐺) ∈ 𝐵) |
93 | 92 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 ∙ 𝐺) ∈ 𝐵) |
94 | | simprrl 804 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵) |
95 | 2, 22 | ringcl 18561 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Ring ∧ 𝑑 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑑 ∙ 𝐺) ∈ 𝐵) |
96 | 85, 94, 87, 95 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵) |
97 | 96 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵) |
98 | | simp2rr 1131 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁) |
99 | | simp31 1097 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))) |
100 | 99 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
101 | 12 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring) |
102 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉) = (𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉) |
103 | | snfi 8038 |
. . . . . . . . . . . . . 14
⊢ {𝑒} ∈ Fin |
104 | 103 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin) |
105 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin) |
106 | 1, 3, 2 | matbas2i 20228 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝐵 → 𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
107 | 90, 106 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
108 | | simprrr 805 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁) |
109 | 108 | snssd 4340 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ⊆ 𝑁) |
110 | | xpss1 5228 |
. . . . . . . . . . . . . . 15
⊢ ({𝑒} ⊆ 𝑁 → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) |
112 | | elmapssres 7882 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁))) |
113 | 107, 111,
112 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁))) |
114 | 1, 3, 2 | matbas2i 20228 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ 𝐵 → 𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
115 | 94, 114 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
116 | | elmapssres 7882 |
. . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁))) |
117 | 115, 111,
116 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁))) |
118 | 66 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
119 | 3, 101, 102, 104, 105, 105, 6, 113, 117, 118 | mamudi 20209 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) ∘𝑓
(+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺))) |
120 | 119 | 3adant3 1081 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) ∘𝑓
(+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺))) |
121 | 100, 120 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) ∘𝑓
(+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺))) |
122 | 56 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = ∙ ) |
123 | 122 | oveqd 6667 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) = (𝑏 ∙ 𝐺)) |
124 | 123 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) |
125 | | simpl1 1064 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing) |
126 | 86, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
127 | 53, 102, 3, 125, 105, 105, 105, 109, 126, 118 | mamures 20196 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
128 | 124, 127 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
129 | 128 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
130 | 122 | oveqd 6667 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) = (𝑐 ∙ 𝐺)) |
131 | 130 | reseq1d 5395 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) |
132 | 53, 102, 3, 125, 105, 105, 105, 109, 107, 118 | mamures 20196 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
133 | 131, 132 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
134 | 122 | oveqd 6667 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) = (𝑑 ∙ 𝐺)) |
135 | 134 | reseq1d 5395 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) |
136 | 53, 102, 3, 125, 105, 105, 105, 109, 115, 118 | mamures 20196 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
137 | 135, 136 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
138 | 133, 137 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) ∘𝑓
(+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺))) |
139 | 138 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) ∘𝑓
(+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺))) |
140 | 121, 129,
139 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))) |
141 | | simp32 1098 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
142 | 141 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
143 | 123 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
144 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉) = (𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉) |
145 | | difssd 3738 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁) |
146 | 53, 144, 3, 125, 105, 105, 105, 145, 126, 118 | mamures 20196 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
147 | 143, 146 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
148 | 147 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
149 | 130 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
150 | 53, 144, 3, 125, 105, 105, 105, 145, 107, 118 | mamures 20196 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
151 | 149, 150 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
152 | 151 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
153 | 142, 148,
152 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
154 | | simp33 1099 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
155 | 154 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
156 | 134 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
157 | 53, 144, 3, 125, 105, 105, 105, 145, 115, 118 | mamures 20196 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
158 | 156, 157 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
159 | 158 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
160 | 155, 148,
159 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
161 | 13, 1, 2, 6, 84, 89, 93, 97, 98, 140, 153, 160 | mdetrlin 20408 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = ((𝐷‘(𝑐 ∙ 𝐺))(+g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺)))) |
162 | 86, 32 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺))) |
163 | 162 | 3adant3 1081 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺))) |
164 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (𝑎 ∙ 𝐺) = (𝑐 ∙ 𝐺)) |
165 | 164 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑐 ∙ 𝐺))) |
166 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝐷‘(𝑐 ∙ 𝐺)) ∈ V |
167 | 165, 26, 166 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺))) |
168 | 90, 167 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺))) |
169 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑑 → (𝑎 ∙ 𝐺) = (𝑑 ∙ 𝐺)) |
170 | 169 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑑 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑑 ∙ 𝐺))) |
171 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝐷‘(𝑑 ∙ 𝐺)) ∈ V |
172 | 170, 26, 171 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺))) |
173 | 94, 172 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺))) |
174 | 168, 173 | oveq12d 6668 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺)))) |
175 | 174 | 3adant3 1081 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺)))) |
176 | 161, 163,
175 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))) |
177 | 176 | 3expia 1267 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
178 | 177 | anassrs 680 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
179 | 178 | ralrimivva 2971 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
180 | 179 | ralrimivva 2971 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓
(+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
181 | | simp11 1091 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing) |
182 | 18 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring) |
183 | | simprll 802 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵) |
184 | | simpl3 1066 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵) |
185 | 182, 183,
184, 38 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵) |
186 | 185 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵) |
187 | | simp2lr 1129 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐 ∈ (Base‘𝑅)) |
188 | | simprrl 804 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵) |
189 | 182, 188,
184, 95 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵) |
190 | 189 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵) |
191 | | simp2rr 1131 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁) |
192 | | simp3l 1089 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))) |
193 | 192 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
194 | 56 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = ∙ ) |
195 | 194 | oveqd 6667 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) = (𝑏 ∙ 𝐺)) |
196 | 195 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) |
197 | | simpl1 1064 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing) |
198 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin) |
199 | | simprrr 805 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁) |
200 | 199 | snssd 4340 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ⊆ 𝑁) |
201 | 183, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
202 | 66 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
203 | 53, 102, 3, 197, 198, 198, 198, 200, 201, 202 | mamures 20196 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
204 | 196, 203 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
205 | 204 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
206 | 194 | oveqd 6667 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) = (𝑑 ∙ 𝐺)) |
207 | 206 | reseq1d 5395 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) |
208 | 188, 114 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
209 | 53, 102, 3, 197, 198, 198, 198, 200, 208, 202 | mamures 20196 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
210 | 207, 209 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
211 | 210 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 ·
((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 ·
((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺))) |
212 | 12 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring) |
213 | 103 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin) |
214 | | simprlr 803 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ (Base‘𝑅)) |
215 | 200, 110 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) |
216 | 208, 215,
116 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁))) |
217 | 3, 212, 102, 213, 198, 198, 7, 214, 216, 202 | mamuvs1 20211 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 ·
((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺))) |
218 | 211, 217 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 ·
((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
219 | 218 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 ·
((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul 〈{𝑒}, 𝑁, 𝑁〉)𝐺)) |
220 | 193, 205,
219 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 ·
((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))) |
221 | | simp3r 1090 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
222 | 221 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
223 | 195 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
224 | | difssd 3738 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁) |
225 | 53, 144, 3, 197, 198, 198, 198, 224, 201, 202 | mamures 20196 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
226 | 223, 225 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
227 | 226 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
228 | 206 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
229 | 53, 144, 3, 197, 198, 198, 198, 224, 208, 202 | mamures 20196 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
230 | 228, 229 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
231 | 230 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul 〈(𝑁 ∖ {𝑒}), 𝑁, 𝑁〉)𝐺)) |
232 | 222, 227,
231 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) |
233 | 13, 1, 2, 3, 7, 181, 186, 187, 190, 191, 220, 232 | mdetrsca 20409 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺)))) |
234 | | simp2ll 1128 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏 ∈ 𝐵) |
235 | 234, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺))) |
236 | | simp2rl 1130 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑 ∈ 𝐵) |
237 | 172 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑑 ∈ 𝐵 → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺)))) |
238 | 236, 237 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺)))) |
239 | 233, 235,
238 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))) |
240 | 239 | 3expia 1267 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
241 | 240 | anassrs 680 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
242 | 241 | ralrimivva 2971 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
243 | 242 | ralrimivva 2971 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ (Base‘𝑅)∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))) |
244 | | simp2 1062 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
245 | 1, 2, 3, 4, 5, 6, 7, 10, 12, 27, 83, 180, 243, 13, 52, 244 | mdetuni0 20427 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) · (𝐷‘𝐹))) |
246 | | oveq1 6657 |
. . . . 5
⊢ (𝑎 = 𝐹 → (𝑎 ∙ 𝐺) = (𝐹 ∙ 𝐺)) |
247 | 246 | fveq2d 6195 |
. . . 4
⊢ (𝑎 = 𝐹 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝐹 ∙ 𝐺))) |
248 | | fvex 6201 |
. . . 4
⊢ (𝐷‘(𝐹 ∙ 𝐺)) ∈ V |
249 | 247, 26, 248 | fvmpt 6282 |
. . 3
⊢ (𝐹 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺))) |
250 | 249 | 3ad2ant2 1083 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺))) |
251 | | eqid 2622 |
. . . . . . 7
⊢
(1r‘𝐴) = (1r‘𝐴) |
252 | 2, 251 | ringidcl 18568 |
. . . . . 6
⊢ (𝐴 ∈ Ring →
(1r‘𝐴)
∈ 𝐵) |
253 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑎 = (1r‘𝐴) → (𝑎 ∙ 𝐺) = ((1r‘𝐴) ∙ 𝐺)) |
254 | 253 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑎 = (1r‘𝐴) → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘((1r‘𝐴) ∙ 𝐺))) |
255 | | fvex 6201 |
. . . . . . 7
⊢ (𝐷‘((1r‘𝐴) ∙ 𝐺)) ∈ V |
256 | 254, 26, 255 | fvmpt 6282 |
. . . . . 6
⊢
((1r‘𝐴) ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) = (𝐷‘((1r‘𝐴) ∙ 𝐺))) |
257 | 18, 252, 256 | 3syl 18 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) = (𝐷‘((1r‘𝐴) ∙ 𝐺))) |
258 | | simp3 1063 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
259 | 2, 22, 251 | ringlidm 18571 |
. . . . . . 7
⊢ ((𝐴 ∈ Ring ∧ 𝐺 ∈ 𝐵) → ((1r‘𝐴) ∙ 𝐺) = 𝐺) |
260 | 18, 258, 259 | syl2anc 693 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((1r‘𝐴) ∙ 𝐺) = 𝐺) |
261 | 260 | fveq2d 6195 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((1r‘𝐴) ∙ 𝐺)) = (𝐷‘𝐺)) |
262 | 257, 261 | eqtrd 2656 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) = (𝐷‘𝐺)) |
263 | 262 | oveq1d 6665 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐺) · (𝐷‘𝐹))) |
264 | 15, 258 | ffvelrnd 6360 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) ∈ (Base‘𝑅)) |
265 | 15, 244 | ffvelrnd 6360 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐹) ∈ (Base‘𝑅)) |
266 | 3, 7 | crngcom 18562 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝐷‘𝐺) ∈ (Base‘𝑅) ∧ (𝐷‘𝐹) ∈ (Base‘𝑅)) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺))) |
267 | 52, 264, 265, 266 | syl3anc 1326 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺))) |
268 | 263, 267 | eqtrd 2656 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺))) |
269 | 245, 250,
268 | 3eqtr3d 2664 |
1
⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺))) |