Step |
Hyp |
Ref |
Expression |
1 |
|
mavmuldm.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
mavmuldm.c |
⊢ 𝐶 = ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) |
3 |
|
mavmuldm.d |
⊢ 𝐷 = ( 𝐵 ↑m 𝑁 ) |
4 |
|
mavmuldm.t |
⊢ · = ( 𝑅 maVecMul 〈 𝑀 , 𝑁 〉 ) |
5 |
|
mavmulsolcl.e |
⊢ 𝐸 = ( 𝐵 ↑m 𝑀 ) |
6 |
|
2a1 |
⊢ ( 𝑋 ∈ 𝐷 → ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) ) |
7 |
|
simpl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) → 𝑅 ∈ 𝑉 ) |
8 |
7
|
adantl |
⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑅 ∈ 𝑉 ) |
9 |
|
simpl1 |
⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑀 ∈ Fin ) |
10 |
|
simpl2 |
⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑁 ∈ Fin ) |
11 |
8 9 10
|
3jca |
⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) ) |
12 |
11
|
adantl |
⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) ) |
13 |
1 2 3 4
|
mavmuldm |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → dom · = ( 𝐶 × 𝐷 ) ) |
14 |
12 13
|
syl |
⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → dom · = ( 𝐶 × 𝐷 ) ) |
15 |
|
simpl |
⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ¬ 𝑋 ∈ 𝐷 ) |
16 |
15
|
intnand |
⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ¬ ( 𝐴 ∈ 𝐶 ∧ 𝑋 ∈ 𝐷 ) ) |
17 |
|
ndmovg |
⊢ ( ( dom · = ( 𝐶 × 𝐷 ) ∧ ¬ ( 𝐴 ∈ 𝐶 ∧ 𝑋 ∈ 𝐷 ) ) → ( 𝐴 · 𝑋 ) = ∅ ) |
18 |
14 16 17
|
syl2anc |
⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( 𝐴 · 𝑋 ) = ∅ ) |
19 |
|
eqeq1 |
⊢ ( ( 𝐴 · 𝑋 ) = ∅ → ( ( 𝐴 · 𝑋 ) = 𝑌 ↔ ∅ = 𝑌 ) ) |
20 |
|
elmapi |
⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝑀 ) → 𝑌 : 𝑀 ⟶ 𝐵 ) |
21 |
|
f0dom0 |
⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑀 = ∅ ↔ 𝑌 = ∅ ) ) |
22 |
21
|
biimprd |
⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑌 = ∅ → 𝑀 = ∅ ) ) |
23 |
22
|
necon3d |
⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑀 ≠ ∅ → 𝑌 ≠ ∅ ) ) |
24 |
23
|
com12 |
⊢ ( 𝑀 ≠ ∅ → ( 𝑌 : 𝑀 ⟶ 𝐵 → 𝑌 ≠ ∅ ) ) |
25 |
24
|
3ad2ant3 |
⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → ( 𝑌 : 𝑀 ⟶ 𝐵 → 𝑌 ≠ ∅ ) ) |
26 |
25
|
com12 |
⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) |
27 |
26
|
a1d |
⊢ ( 𝑌 : 𝑀 ⟶ 𝐵 → ( 𝑅 ∈ 𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) ) |
28 |
20 27
|
syl |
⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝑀 ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) ) |
29 |
28 5
|
eleq2s |
⊢ ( 𝑌 ∈ 𝐸 → ( 𝑅 ∈ 𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) ) |
30 |
29
|
impcom |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) |
31 |
30
|
impcom |
⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → 𝑌 ≠ ∅ ) |
32 |
|
eqneqall |
⊢ ( 𝑌 = ∅ → ( 𝑌 ≠ ∅ → 𝑋 ∈ 𝐷 ) ) |
33 |
31 32
|
syl5com |
⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( 𝑌 = ∅ → 𝑋 ∈ 𝐷 ) ) |
34 |
33
|
adantl |
⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( 𝑌 = ∅ → 𝑋 ∈ 𝐷 ) ) |
35 |
34
|
com12 |
⊢ ( 𝑌 = ∅ → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → 𝑋 ∈ 𝐷 ) ) |
36 |
35
|
eqcoms |
⊢ ( ∅ = 𝑌 → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → 𝑋 ∈ 𝐷 ) ) |
37 |
19 36
|
syl6bi |
⊢ ( ( 𝐴 · 𝑋 ) = ∅ → ( ( 𝐴 · 𝑋 ) = 𝑌 → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → 𝑋 ∈ 𝐷 ) ) ) |
38 |
37
|
com23 |
⊢ ( ( 𝐴 · 𝑋 ) = ∅ → ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) ) |
39 |
18 38
|
mpcom |
⊢ ( ( ¬ 𝑋 ∈ 𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) |
40 |
39
|
ex |
⊢ ( ¬ 𝑋 ∈ 𝐷 → ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) ) |
41 |
6 40
|
pm2.61i |
⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌 → 𝑋 ∈ 𝐷 ) ) |