Proof of Theorem cramer0
Step | Hyp | Ref
| Expression |
1 | | cramer.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐴) |
2 | | cramer.a |
. . . . . . . . . 10
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | 2 | fveq2i 6771 |
. . . . . . . . 9
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
4 | 1, 3 | eqtri 2767 |
. . . . . . . 8
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
5 | | fvoveq1 7291 |
. . . . . . . 8
⊢ (𝑁 = ∅ →
(Base‘(𝑁 Mat 𝑅)) = (Base‘(∅ Mat
𝑅))) |
6 | 4, 5 | eqtrid 2791 |
. . . . . . 7
⊢ (𝑁 = ∅ → 𝐵 = (Base‘(∅ Mat
𝑅))) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → 𝐵 = (Base‘(∅ Mat
𝑅))) |
8 | 7 | eleq2d 2825 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (Base‘(∅ Mat 𝑅)))) |
9 | | mat0dimbas0 21596 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
(Base‘(∅ Mat 𝑅)) = {∅}) |
10 | 9 | eleq2d 2825 |
. . . . . 6
⊢ (𝑅 ∈ CRing → (𝑋 ∈ (Base‘(∅ Mat
𝑅)) ↔ 𝑋 ∈
{∅})) |
11 | 10 | adantl 481 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑋 ∈ (Base‘(∅ Mat
𝑅)) ↔ 𝑋 ∈
{∅})) |
12 | 8, 11 | bitrd 278 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ {∅})) |
13 | | cramer.v |
. . . . . . . 8
⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → 𝑉 = ((Base‘𝑅) ↑m 𝑁)) |
15 | | oveq2 7276 |
. . . . . . . 8
⊢ (𝑁 = ∅ →
((Base‘𝑅)
↑m 𝑁) =
((Base‘𝑅)
↑m ∅)) |
16 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑m 𝑁) =
((Base‘𝑅)
↑m ∅)) |
17 | | fvex 6781 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
18 | | map0e 8644 |
. . . . . . . 8
⊢
((Base‘𝑅)
∈ V → ((Base‘𝑅) ↑m ∅) =
1o) |
19 | 17, 18 | mp1i 13 |
. . . . . . 7
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑m ∅) = 1o) |
20 | 14, 16, 19 | 3eqtrd 2783 |
. . . . . 6
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → 𝑉 =
1o) |
21 | 20 | eleq2d 2825 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑌 ∈ 𝑉 ↔ 𝑌 ∈ 1o)) |
22 | | el1o 8305 |
. . . . 5
⊢ (𝑌 ∈ 1o ↔
𝑌 =
∅) |
23 | 21, 22 | bitrdi 286 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑌 ∈ 𝑉 ↔ 𝑌 = ∅)) |
24 | 12, 23 | anbi12d 630 |
. . 3
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ↔ (𝑋 ∈ {∅} ∧ 𝑌 = ∅))) |
25 | | elsni 4583 |
. . . 4
⊢ (𝑋 ∈ {∅} → 𝑋 = ∅) |
26 | | mpteq1 5171 |
. . . . . . . . . 10
⊢ (𝑁 = ∅ → (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) = (𝑖 ∈ ∅ ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) |
27 | | mpt0 6571 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ∅ ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) = ∅ |
28 | 26, 27 | eqtrdi 2795 |
. . . . . . . . 9
⊢ (𝑁 = ∅ → (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) = ∅) |
29 | 28 | eqeq2d 2750 |
. . . . . . . 8
⊢ (𝑁 = ∅ → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ 𝑍 = ∅)) |
30 | 29 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ 𝑍 = ∅)) |
31 | | simplrl 773 |
. . . . . . . . . 10
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → 𝑋 = ∅) |
32 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → 𝑍 = ∅) |
33 | 31, 32 | oveq12d 7286 |
. . . . . . . . 9
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → (𝑋 · 𝑍) = (∅ ·
∅)) |
34 | | cramer.x |
. . . . . . . . . . 11
⊢ · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) |
35 | 34 | mavmul0 21682 |
. . . . . . . . . 10
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (∅
·
∅) = ∅) |
36 | 35 | ad2antrr 722 |
. . . . . . . . 9
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → (∅
·
∅) = ∅) |
37 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑋 = ∅ ∧ 𝑌 = ∅) → 𝑌 = ∅) |
38 | 37 | eqcomd 2745 |
. . . . . . . . . 10
⊢ ((𝑋 = ∅ ∧ 𝑌 = ∅) → ∅ =
𝑌) |
39 | 38 | ad2antlr 723 |
. . . . . . . . 9
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → ∅ =
𝑌) |
40 | 33, 36, 39 | 3eqtrd 2783 |
. . . . . . . 8
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → (𝑋 · 𝑍) = 𝑌) |
41 | 40 | ex 412 |
. . . . . . 7
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → (𝑍 = ∅ → (𝑋 · 𝑍) = 𝑌)) |
42 | 30, 41 | sylbid 239 |
. . . . . 6
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |
43 | 42 | a1d 25 |
. . . . 5
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))) |
44 | 43 | ex 412 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 = ∅ ∧ 𝑌 = ∅) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)))) |
45 | 25, 44 | sylani 603 |
. . 3
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 ∈ {∅} ∧ 𝑌 = ∅) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)))) |
46 | 24, 45 | sylbid 239 |
. 2
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)))) |
47 | 46 | 3imp 1109 |
1
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |