Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2610 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (1r‘𝑅) |
3 | 1, 2 | ringidcl 18391 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
4 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | 1, 4 | ring0cl 18392 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
6 | 3, 5 | ifcld 4081 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅)) |
7 | 6 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅)) |
8 | | eqid 2610 |
. . . . . 6
⊢ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) = (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) |
9 | 7, 8 | fmptd 6292 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))):𝐼⟶(Base‘𝑅)) |
10 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
11 | | elmapg 7757 |
. . . . . . 7
⊢
(((Base‘𝑅)
∈ V ∧ 𝐼 ∈
𝑊) → ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))):𝐼⟶(Base‘𝑅))) |
12 | 10, 11 | mpan 702 |
. . . . . 6
⊢ (𝐼 ∈ 𝑊 → ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))):𝐼⟶(Base‘𝑅))) |
13 | 12 | ad2antlr 759 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))):𝐼⟶(Base‘𝑅))) |
14 | 9, 13 | mpbird 246 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑𝑚 𝐼)) |
15 | | mptexg 6389 |
. . . . . 6
⊢ (𝐼 ∈ 𝑊 → (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ V) |
16 | 15 | ad2antlr 759 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ V) |
17 | | funmpt 5840 |
. . . . . 6
⊢ Fun
(𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) |
18 | 17 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → Fun (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))) |
19 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑅) ∈ V |
20 | 19 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → (0g‘𝑅) ∈ V) |
21 | | snfi 7923 |
. . . . . 6
⊢ {𝑖} ∈ Fin |
22 | 21 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → {𝑖} ∈ Fin) |
23 | | eldifsni 4261 |
. . . . . . . . 9
⊢ (𝑗 ∈ (𝐼 ∖ {𝑖}) → 𝑗 ≠ 𝑖) |
24 | 23 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ (𝐼 ∖ {𝑖})) → 𝑗 ≠ 𝑖) |
25 | 24 | neneqd 2787 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ (𝐼 ∖ {𝑖})) → ¬ 𝑗 = 𝑖) |
26 | 25 | iffalsed 4047 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ (𝐼 ∖ {𝑖})) → if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
27 | | simplr 788 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
28 | 26, 27 | suppss2 7216 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) supp (0g‘𝑅)) ⊆ {𝑖}) |
29 | | suppssfifsupp 8173 |
. . . . 5
⊢ ((((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ V ∧ Fun (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∧ (0g‘𝑅) ∈ V) ∧ ({𝑖} ∈ Fin ∧ ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) supp (0g‘𝑅)) ⊆ {𝑖})) → (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) finSupp (0g‘𝑅)) |
30 | 16, 18, 20, 22, 28, 29 | syl32anc 1326 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) finSupp (0g‘𝑅)) |
31 | | uvcff.y |
. . . . . 6
⊢ 𝑌 = (𝑅 freeLMod 𝐼) |
32 | | uvcff.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑌) |
33 | 31, 1, 4, 32 | frlmelbas 19919 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐵 ↔ ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∧ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) finSupp (0g‘𝑅)))) |
34 | 33 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐵 ↔ ((𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∧ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) finSupp (0g‘𝑅)))) |
35 | 14, 30, 34 | mpbir2and 959 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐵) |
36 | | eqid 2610 |
. . 3
⊢ (𝑖 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))) = (𝑖 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))) |
37 | 35, 36 | fmptd 6292 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → (𝑖 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))):𝐼⟶𝐵) |
38 | | uvcff.u |
. . . 4
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
39 | 38, 2, 4 | uvcfval 19942 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝑈 = (𝑖 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))))) |
40 | 39 | feq1d 5943 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → (𝑈:𝐼⟶𝐵 ↔ (𝑖 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))):𝐼⟶𝐵)) |
41 | 37, 40 | mpbird 246 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝑈:𝐼⟶𝐵) |