Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aacllem Structured version   Visualization version   GIF version

Theorem aacllem 47334
Description: Lemma for other theorems about 𝔸. (Contributed by Brendan Leahy, 3-Jan-2020.) (Revised by Alexander van der Vekens and David A. Wheeler, 25-Apr-2020.)
Hypotheses
Ref Expression
aacllem.0 (πœ‘ β†’ 𝐴 ∈ β„‚)
aacllem.1 (πœ‘ β†’ 𝑁 ∈ β„•0)
aacllem.2 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
aacllem.3 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
aacllem.4 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β†‘π‘˜) = Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋))
Assertion
Ref Expression
aacllem (πœ‘ β†’ 𝐴 ∈ 𝔸)
Distinct variable groups:   𝐴,π‘˜,𝑛   π‘˜,𝑁,𝑛   π‘˜,𝑋   πœ‘,π‘˜,𝑛
Allowed substitution hints:   𝐢(π‘˜,𝑛)   𝑋(𝑛)

Proof of Theorem aacllem
Dummy variables 𝑀 π‘₯ 𝑦 𝐡 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 aacllem.0 . 2 (πœ‘ β†’ 𝐴 ∈ β„‚)
2 aacllem.1 . . . . . . 7 (πœ‘ β†’ 𝑁 ∈ β„•0)
32nn0red 12479 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ)
43ltp1d 12090 . . . . 5 (πœ‘ β†’ 𝑁 < (𝑁 + 1))
5 peano2nn0 12458 . . . . . . . 8 (𝑁 ∈ β„•0 β†’ (𝑁 + 1) ∈ β„•0)
62, 5syl 17 . . . . . . 7 (πœ‘ β†’ (𝑁 + 1) ∈ β„•0)
76nn0red 12479 . . . . . 6 (πœ‘ β†’ (𝑁 + 1) ∈ ℝ)
83, 7ltnled 11307 . . . . 5 (πœ‘ β†’ (𝑁 < (𝑁 + 1) ↔ Β¬ (𝑁 + 1) ≀ 𝑁))
94, 8mpbid 231 . . . 4 (πœ‘ β†’ Β¬ (𝑁 + 1) ≀ 𝑁)
10 aacllem.3 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
11103expa 1119 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
1211fmpttd 7064 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
13 qex 12891 . . . . . . . . . . 11 β„š ∈ V
14 ovex 7391 . . . . . . . . . . 11 (1...𝑁) ∈ V
1513, 14elmap 8812 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
1612, 15sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
1716fmpttd 7064 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)⟢(β„š ↑m (1...𝑁)))
18 eqid 2733 . . . . . . . . . . . 12 (β„‚fld β†Ύs β„š) = (β„‚fld β†Ύs β„š)
1918qdrng 26984 . . . . . . . . . . 11 (β„‚fld β†Ύs β„š) ∈ DivRing
20 drngring 20204 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ Ring)
2119, 20ax-mp 5 . . . . . . . . . 10 (β„‚fld β†Ύs β„š) ∈ Ring
22 fzfi 13883 . . . . . . . . . 10 (1...𝑁) ∈ Fin
23 eqid 2733 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) = ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))
2423frlmlmod 21171 . . . . . . . . . 10 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod)
2521, 22, 24mp2an 691 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod
26 fzfi 13883 . . . . . . . . 9 (0...𝑁) ∈ Fin
2718qrngbas 26983 . . . . . . . . . . . 12 β„š = (Baseβ€˜(β„‚fld β†Ύs β„š))
2823, 27frlmfibas 21184 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (1...𝑁) ∈ Fin) β†’ (β„š ↑m (1...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
2919, 22, 28mp2an 691 . . . . . . . . . 10 (β„š ↑m (1...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
3023frlmsca 21175 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (1...𝑁) ∈ Fin) β†’ (β„‚fld β†Ύs β„š) = (Scalarβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
3119, 22, 30mp2an 691 . . . . . . . . . 10 (β„‚fld β†Ύs β„š) = (Scalarβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
32 eqid 2733 . . . . . . . . . 10 ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
3318qrng0 26985 . . . . . . . . . . . 12 0 = (0gβ€˜(β„‚fld β†Ύs β„š))
3423, 33frlm0 21176 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((1...𝑁) Γ— {0}) = (0gβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
3521, 22, 34mp2an 691 . . . . . . . . . 10 ((1...𝑁) Γ— {0}) = (0gβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
36 eqid 2733 . . . . . . . . . . . 12 ((β„‚fld β†Ύs β„š) freeLMod (0...𝑁)) = ((β„‚fld β†Ύs β„š) freeLMod (0...𝑁))
3736, 27frlmfibas 21184 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (0...𝑁) ∈ Fin) β†’ (β„š ↑m (0...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (0...𝑁))))
3819, 26, 37mp2an 691 . . . . . . . . . 10 (β„š ↑m (0...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (0...𝑁)))
3929, 31, 32, 35, 33, 38islindf4 21260 . . . . . . . . 9 ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (0...𝑁) ∈ Fin ∧ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)⟢(β„š ↑m (1...𝑁))) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
4025, 26, 39mp3an12 1452 . . . . . . . 8 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)⟢(β„š ↑m (1...𝑁)) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
4117, 40syl 17 . . . . . . 7 (πœ‘ β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
42 elmapi 8790 . . . . . . . . 9 (𝑀 ∈ (β„š ↑m (0...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
43 fzfid 13884 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (0...𝑁) ∈ Fin)
44 fvexd 6858 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
4514mptex 7174 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V
4645a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V)
47 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
4847feqmptd 6911 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀 = (π‘˜ ∈ (0...𝑁) ↦ (π‘€β€˜π‘˜)))
49 eqidd 2734 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
5043, 44, 46, 48, 49offval2 7638 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢))))
51 fzfid 13884 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (1...𝑁) ∈ Fin)
52 ffvelcdm 7033 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5352adantll 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5416adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
55 cnfldmul 20818 . . . . . . . . . . . . . . . . . . . . . 22 Β· = (.rβ€˜β„‚fld)
5618, 55ressmulr 17193 . . . . . . . . . . . . . . . . . . . . 21 (β„š ∈ V β†’ Β· = (.rβ€˜(β„‚fld β†Ύs β„š)))
5713, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Β· = (.rβ€˜(β„‚fld β†Ύs β„š))
5823, 29, 27, 51, 53, 54, 32, 57frlmvscafval 21188 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
59 fvexd 6858 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
6011adantllr 718 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
61 fconstmpt 5695 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜))
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜)))
63 eqidd 2734 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) = (𝑛 ∈ (1...𝑁) ↦ 𝐢))
6451, 59, 60, 62, 63offval2 7638 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6558, 64eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6665mpteq2dva 5206 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
6750, 66eqtrd 2773 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
6867oveq2d 7374 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
69 fzfid 13884 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (1...𝑁) ∈ Fin)
7021a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (β„‚fld β†Ύs β„š) ∈ Ring)
7153adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
7211an32s 651 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„š)
7372adantllr 718 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„š)
74 qmulcl 12897 . . . . . . . . . . . . . . . . . . . 20 (((π‘€β€˜π‘˜) ∈ β„š ∧ 𝐢 ∈ β„š) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7571, 73, 74syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7675an32s 651 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7776fmpttd 7064 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7813, 14elmap 8812 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7977, 78sylibr 233 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)))
80 eqid 2733 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
8114mptex 7174 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V)
83 snex 5389 . . . . . . . . . . . . . . . . . . 19 {0} ∈ V
8414, 83xpex 7688 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) Γ— {0}) ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((1...𝑁) Γ— {0}) ∈ V)
8680, 43, 82, 85fsuppmptdm 9321 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) finSupp ((1...𝑁) Γ— {0}))
8723, 29, 35, 69, 43, 70, 79, 86frlmgsum 21194 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
88 cnfldbas 20816 . . . . . . . . . . . . . . . . . 18 β„‚ = (Baseβ€˜β„‚fld)
89 cnfldadd 20817 . . . . . . . . . . . . . . . . . 18 + = (+gβ€˜β„‚fld)
90 cnfldex 20815 . . . . . . . . . . . . . . . . . . 19 β„‚fld ∈ V
9190a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„‚fld ∈ V)
92 fzfid 13884 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (0...𝑁) ∈ Fin)
93 qsscn 12890 . . . . . . . . . . . . . . . . . . 19 β„š βŠ† β„‚
9493a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„š βŠ† β„‚)
9575fmpttd 7064 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(0...𝑁)βŸΆβ„š)
96 0z 12515 . . . . . . . . . . . . . . . . . . . 20 0 ∈ β„€
97 zq 12884 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„€ β†’ 0 ∈ β„š)
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . 19 0 ∈ β„š
9998a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 0 ∈ β„š)
100 addid2 11343 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (0 + π‘₯) = π‘₯)
101 addid1 11340 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (π‘₯ + 0) = π‘₯)
102100, 101jca 513 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ β„‚ β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
103102adantl 483 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ β„‚) β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
10488, 89, 18, 91, 92, 94, 95, 99, 103gsumress 18542 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
105 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
106 qcn 12893 . . . . . . . . . . . . . . . . . . . . 21 ((π‘€β€˜π‘˜) ∈ β„š β†’ (π‘€β€˜π‘˜) ∈ β„‚)
10752, 106syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
108105, 107sylan 581 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
109 qcn 12893 . . . . . . . . . . . . . . . . . . . . . 22 (𝐢 ∈ β„š β†’ 𝐢 ∈ β„‚)
11011, 109syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„‚)
111110an32s 651 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
112111adantllr 718 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
113108, 112mulcld 11180 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
11492, 113gsumfsum 20880 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
115104, 114eqtr3d 2775 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
116115mpteq2dva 5206 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)))
11768, 87, 1163eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)))
118 qaddcl 12895 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š) β†’ (π‘₯ + 𝑦) ∈ β„š)
119118adantl 483 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ (π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š)) β†’ (π‘₯ + 𝑦) ∈ β„š)
12094, 119, 92, 75, 99fsumcllem 15622 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
121120fmpttd 7064 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
12213, 14elmap 8812 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
123121, 122sylibr 233 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)))
124117, 123eqeltrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) ∈ (β„š ↑m (1...𝑁)))
125 elmapi 8790 . . . . . . . . . . . . 13 ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) ∈ (β„š ↑m (1...𝑁)) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))):(1...𝑁)βŸΆβ„š)
126 ffn 6669 . . . . . . . . . . . . 13 ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))):(1...𝑁)βŸΆβ„š β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) Fn (1...𝑁))
127124, 125, 1263syl 18 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) Fn (1...𝑁))
128 c0ex 11154 . . . . . . . . . . . . 13 0 ∈ V
129 fnconstg 6731 . . . . . . . . . . . . 13 (0 ∈ V β†’ ((1...𝑁) Γ— {0}) Fn (1...𝑁))
130128, 129ax-mp 5 . . . . . . . . . . . 12 ((1...𝑁) Γ— {0}) Fn (1...𝑁)
131 nfcv 2904 . . . . . . . . . . . . . 14 Ⅎ𝑛((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))
132 nfcv 2904 . . . . . . . . . . . . . 14 Ⅎ𝑛 Ξ£g
133 nfcv 2904 . . . . . . . . . . . . . . 15 Ⅎ𝑛𝑀
134 nfcv 2904 . . . . . . . . . . . . . . 15 Ⅎ𝑛 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
135 nfcv 2904 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(0...𝑁)
136 nfmpt1 5214 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐢)
137135, 136nfmpt 5213 . . . . . . . . . . . . . . 15 Ⅎ𝑛(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
138133, 134, 137nfov 7388 . . . . . . . . . . . . . 14 Ⅎ𝑛(𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
139131, 132, 138nfov 7388 . . . . . . . . . . . . 13 Ⅎ𝑛(((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))
140 nfcv 2904 . . . . . . . . . . . . 13 Ⅎ𝑛((1...𝑁) Γ— {0})
141139, 140eqfnfv2f 6987 . . . . . . . . . . . 12 (((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) Fn (1...𝑁) ∧ ((1...𝑁) Γ— {0}) Fn (1...𝑁)) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) ↔ βˆ€π‘› ∈ (1...𝑁)((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = (((1...𝑁) Γ— {0})β€˜π‘›)))
142127, 130, 141sylancl 587 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) ↔ βˆ€π‘› ∈ (1...𝑁)((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = (((1...𝑁) Γ— {0})β€˜π‘›)))
143117fveq1d 6845 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›))
144 sumex 15578 . . . . . . . . . . . . . . 15 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ V
145 eqid 2733 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
146145fvmpt2 6960 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ V) β†’ ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
147144, 146mpan2 690 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
148143, 147sylan9eq 2793 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
149128fvconst2 7154 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {0})β€˜π‘›) = 0)
150149adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((1...𝑁) Γ— {0})β€˜π‘›) = 0)
151148, 150eqeq12d 2749 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = (((1...𝑁) Γ— {0})β€˜π‘›) ↔ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
152151ralbidva 3169 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (βˆ€π‘› ∈ (1...𝑁)((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = (((1...𝑁) Γ— {0})β€˜π‘›) ↔ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
153142, 152bitrd 279 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) ↔ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
154153imbi1d 342 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ (βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
15542, 154sylan2 594 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (β„š ↑m (0...𝑁))) β†’ (((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ (βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
156155ralbidva 3169 . . . . . . 7 (πœ‘ β†’ (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = ((1...𝑁) Γ— {0}) β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
15741, 156bitrd 279 . . . . . 6 (πœ‘ β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
158 drngnzr 20748 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ NzRing)
15919, 158ax-mp 5 . . . . . . . 8 (β„‚fld β†Ύs β„š) ∈ NzRing
16031islindf3 21248 . . . . . . . 8 ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ NzRing) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))))
16125, 159, 160mp2an 691 . . . . . . 7 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
162 eqid 2733 . . . . . . . . . 10 (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
16345, 162dmmpti 6646 . . . . . . . . 9 dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (0...𝑁)
164 f1eq2 6735 . . . . . . . . 9 (dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (0...𝑁) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))–1-1β†’V ↔ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V))
165163, 164ax-mp 5 . . . . . . . 8 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))–1-1β†’V ↔ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V)
166165anbi1i 625 . . . . . . 7 (((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) ↔ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
167161, 166bitri 275 . . . . . 6 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
168 con34b 316 . . . . . . . . 9 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ (Β¬ 𝑀 = ((0...𝑁) Γ— {0}) β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
169 df-nel 3047 . . . . . . . . . . 11 (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} ↔ Β¬ 𝑀 ∈ {((0...𝑁) Γ— {0})})
170 velsn 4603 . . . . . . . . . . 11 (𝑀 ∈ {((0...𝑁) Γ— {0})} ↔ 𝑀 = ((0...𝑁) Γ— {0}))
171169, 170xchbinx 334 . . . . . . . . . 10 (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} ↔ Β¬ 𝑀 = ((0...𝑁) Γ— {0}))
172171imbi1i 350 . . . . . . . . 9 ((𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ↔ (Β¬ 𝑀 = ((0...𝑁) Γ— {0}) β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
173168, 172bitr4i 278 . . . . . . . 8 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
174173ralbii 3093 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
175 raldifb 4105 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ↔ βˆ€π‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
176 ralnex 3072 . . . . . . 7 (βˆ€π‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ↔ Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
177174, 175, 1763bitri 297 . . . . . 6 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
178157, 167, 1773bitr3g 313 . . . . 5 (πœ‘ β†’ (((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) ↔ Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
179 eqid 2733 . . . . . . . . . . . . 13 (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
18029, 179lssmre 20442 . . . . . . . . . . . 12 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod β†’ (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∈ (Mooreβ€˜(β„š ↑m (1...𝑁))))
18125, 180ax-mp 5 . . . . . . . . . . 11 (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∈ (Mooreβ€˜(β„š ↑m (1...𝑁)))
182181a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∈ (Mooreβ€˜(β„š ↑m (1...𝑁))))
183 eqid 2733 . . . . . . . . . . . 12 (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
184 eqid 2733 . . . . . . . . . . . 12 (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) = (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
185179, 183, 184mrclsp 20465 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod β†’ (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
18625, 185ax-mp 5 . . . . . . . . . 10 (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
187 eqid 2733 . . . . . . . . . 10 (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) = (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
18831islvec 20580 . . . . . . . . . . . . 13 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec ↔ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ DivRing))
18925, 19, 188mpbir2an 710 . . . . . . . . . . . 12 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec
190179, 186, 29lssacsex 20621 . . . . . . . . . . . . 13 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec β†’ ((LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∈ (ACSβ€˜(β„š ↑m (1...𝑁))) ∧ βˆ€π‘§ ∈ 𝒫 (β„š ↑m (1...𝑁))βˆ€π‘₯ ∈ (β„š ↑m (1...𝑁))βˆ€π‘¦ ∈ (((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {π‘₯})) βˆ– ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜π‘§))π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {𝑦}))))
191190simprd 497 . . . . . . . . . . . 12 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec β†’ βˆ€π‘§ ∈ 𝒫 (β„š ↑m (1...𝑁))βˆ€π‘₯ ∈ (β„š ↑m (1...𝑁))βˆ€π‘¦ ∈ (((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {π‘₯})) βˆ– ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜π‘§))π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {𝑦})))
192189, 191ax-mp 5 . . . . . . . . . . 11 βˆ€π‘§ ∈ 𝒫 (β„š ↑m (1...𝑁))βˆ€π‘₯ ∈ (β„š ↑m (1...𝑁))βˆ€π‘¦ ∈ (((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {π‘₯})) βˆ– ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜π‘§))π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {𝑦}))
193192a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ βˆ€π‘§ ∈ 𝒫 (β„š ↑m (1...𝑁))βˆ€π‘₯ ∈ (β„š ↑m (1...𝑁))βˆ€π‘¦ ∈ (((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {π‘₯})) βˆ– ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜π‘§))π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(𝑧 βˆͺ {𝑦})))
19417frnd 6677 . . . . . . . . . . . 12 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† (β„š ↑m (1...𝑁)))
195 dif0 4333 . . . . . . . . . . . 12 ((β„š ↑m (1...𝑁)) βˆ– βˆ…) = (β„š ↑m (1...𝑁))
196194, 195sseqtrrdi 3996 . . . . . . . . . . 11 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…))
197196adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…))
198 eqid 2733 . . . . . . . . . . . . . . 15 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) = ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
199198, 23, 29uvcff 21213 . . . . . . . . . . . . . 14 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)):(1...𝑁)⟢(β„š ↑m (1...𝑁)))
20021, 22, 199mp2an 691 . . . . . . . . . . . . 13 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)):(1...𝑁)⟢(β„š ↑m (1...𝑁))
201 frn 6676 . . . . . . . . . . . . 13 (((β„‚fld β†Ύs β„š) unitVec (1...𝑁)):(1...𝑁)⟢(β„š ↑m (1...𝑁)) β†’ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βŠ† (β„š ↑m (1...𝑁)))
202200, 201ax-mp 5 . . . . . . . . . . . 12 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βŠ† (β„š ↑m (1...𝑁))
203202, 195sseqtrri 3982 . . . . . . . . . . 11 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…)
204203a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…))
205 un0 4351 . . . . . . . . . . . . . 14 (ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…) = ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
206205fveq2i 6846 . . . . . . . . . . . . 13 ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)) = ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
207 eqid 2733 . . . . . . . . . . . . . . . 16 (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
20823, 198, 207frlmlbs 21219 . . . . . . . . . . . . . . 15 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
20921, 22, 208mp2an 691 . . . . . . . . . . . . . 14 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
21029, 207, 183lbssp 20555 . . . . . . . . . . . . . 14 (ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) β†’ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) = (β„š ↑m (1...𝑁)))
211209, 210ax-mp 5 . . . . . . . . . . . . 13 ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) = (β„š ↑m (1...𝑁))
212206, 211eqtri 2761 . . . . . . . . . . . 12 ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)) = (β„š ↑m (1...𝑁))
213194, 212sseqtrrdi 3996 . . . . . . . . . . 11 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)))
214213adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)))
215 un0 4351 . . . . . . . . . . 11 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆͺ βˆ…) = ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
21625, 159pm3.2i 472 . . . . . . . . . . . . . 14 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ NzRing)
217183, 31lindsind2 21241 . . . . . . . . . . . . . 14 (((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ NzRing) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∧ π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) β†’ Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
218216, 217mp3an1 1449 . . . . . . . . . . . . 13 ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∧ π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) β†’ Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
219218ralrimiva 3140 . . . . . . . . . . . 12 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) β†’ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
220186, 187ismri2 17517 . . . . . . . . . . . . . 14 (((LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∈ (Mooreβ€˜(β„š ↑m (1...𝑁))) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† (β„š ↑m (1...𝑁))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) ↔ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯}))))
221181, 194, 220sylancr 588 . . . . . . . . . . . . 13 (πœ‘ β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) ↔ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯}))))
222221biimpar 479 . . . . . . . . . . . 12 ((πœ‘ ∧ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯}))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
223219, 222sylan2 594 . . . . . . . . . . 11 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
224215, 223eqeltrid 2838 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
225 mptfi 9298 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin)
226 rnfi 9282 . . . . . . . . . . . . 13 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin)
22726, 225, 226mp2b 10 . . . . . . . . . . . 12 ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin
228227orci 864 . . . . . . . . . . 11 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin ∨ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ Fin)
229228a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin ∨ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ Fin))
230182, 186, 187, 193, 197, 204, 214, 224, 229mreexexd 17533 . . . . . . . . 9 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ βˆƒπ‘£ ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))))
231230ex 414 . . . . . . . 8 (πœ‘ β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) β†’ βˆƒπ‘£ ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))))
232 ovex 7391 . . . . . . . . . . . . 13 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
233232rnex 7850 . . . . . . . . . . . 12 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
234 elpwi 4568 . . . . . . . . . . . 12 (𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ 𝑣 βŠ† ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
235 ssdomg 8943 . . . . . . . . . . . 12 (ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V β†’ (𝑣 βŠ† ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))))
236233, 234, 235mpsyl 68 . . . . . . . . . . 11 (𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
237 endomtr 8955 . . . . . . . . . . . . . 14 ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
238237ancoms 460 . . . . . . . . . . . . 13 ((𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
239 f1f1orn 6796 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1-ontoβ†’ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
240 ovex 7391 . . . . . . . . . . . . . . . . 17 (0...𝑁) ∈ V
241240f1oen 8916 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1-ontoβ†’ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β†’ (0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
242239, 241syl 17 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
243 endomtr 8955 . . . . . . . . . . . . . . . . 17 (((0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
244198uvcendim 21269 . . . . . . . . . . . . . . . . . . . 20 (((β„‚fld β†Ύs β„š) ∈ NzRing ∧ (1...𝑁) ∈ Fin) β†’ (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
245159, 22, 244mp2an 691 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
246245ensymi 8947 . . . . . . . . . . . . . . . . . 18 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)
247 domentr 8956 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)) β†’ (0...𝑁) β‰Ό (1...𝑁))
248 hashdom 14285 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) β†’ ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁)))
24926, 22, 248mp2an 691 . . . . . . . . . . . . . . . . . . . 20 ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁))
250 hashfz0 14338 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
2512, 250syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
252 hashfz1 14252 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(1...𝑁)) = 𝑁)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(1...𝑁)) = 𝑁)
254251, 253breq12d 5119 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (𝑁 + 1) ≀ 𝑁))
255249, 254bitr3id 285 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((0...𝑁) β‰Ό (1...𝑁) ↔ (𝑁 + 1) ≀ 𝑁))
256247, 255imbitrid 243 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)) β†’ (𝑁 + 1) ≀ 𝑁))
257246, 256mpan2i 696 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ (𝑁 + 1) ≀ 𝑁))
258243, 257syl5 34 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (𝑁 + 1) ≀ 𝑁))
259258expd 417 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ (𝑁 + 1) ≀ 𝑁)))
260242, 259syl5 34 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ (𝑁 + 1) ≀ 𝑁)))
261260com23 86 . . . . . . . . . . . . 13 (πœ‘ β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
262238, 261syl5 34 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
263262expdimp 454 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
264236, 263sylan2 594 . . . . . . . . . 10 ((πœ‘ ∧ 𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
265264adantrd 493 . . . . . . . . 9 ((πœ‘ ∧ 𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
266265rexlimdva 3149 . . . . . . . 8 (πœ‘ β†’ (βˆƒπ‘£ ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
267231, 266syld 47 . . . . . . 7 (πœ‘ β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
268267impd 412 . . . . . 6 (πœ‘ β†’ ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∧ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V) β†’ (𝑁 + 1) ≀ 𝑁))
269268ancomsd 467 . . . . 5 (πœ‘ β†’ (((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ (𝑁 + 1) ≀ 𝑁))
270178, 269sylbird 260 . . . 4 (πœ‘ β†’ (Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ (𝑁 + 1) ≀ 𝑁))
2719, 270mt3d 148 . . 3 (πœ‘ β†’ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
272 eldifsn 4748 . . . . 5 (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) ↔ (𝑀 ∈ (β„š ↑m (0...𝑁)) ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
27342anim1i 616 . . . . 5 ((𝑀 ∈ (β„š ↑m (0...𝑁)) ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) β†’ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
274272, 273sylbi 216 . . . 4 (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) β†’ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
27593a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ β„š βŠ† β„‚)
2762adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑁 ∈ β„•0)
277275, 276, 53elplyd 25579 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
278277adantrr 716 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
279 uzdisj 13520 . . . . . . . . . . . . . . . . . 18 ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…
2802nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ β„‚)
281 pncan1 11584 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„‚ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
283282oveq2d 7374 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (0...((𝑁 + 1) βˆ’ 1)) = (0...𝑁))
284283ineq1d 4172 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
285279, 284eqtr3id 2787 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ… = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
286285eqcomd 2739 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
287128fconst 6729 . . . . . . . . . . . . . . . . . 18 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0}
288 snssi 4769 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„š β†’ {0} βŠ† β„š)
28996, 97, 288mp2b 10 . . . . . . . . . . . . . . . . . . 19 {0} βŠ† β„š
290289, 93sstri 3954 . . . . . . . . . . . . . . . . . 18 {0} βŠ† β„‚
291 fss 6686 . . . . . . . . . . . . . . . . . 18 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„‚) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚)
292287, 290, 291mp2an 691 . . . . . . . . . . . . . . . . 17 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚
293 fun 6705 . . . . . . . . . . . . . . . . 17 (((𝑀:(0...𝑁)βŸΆβ„š ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
294292, 293mpanl2 700 . . . . . . . . . . . . . . . 16 ((𝑀:(0...𝑁)βŸΆβ„š ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
295286, 294sylan2 594 . . . . . . . . . . . . . . 15 ((𝑀:(0...𝑁)βŸΆβ„š ∧ πœ‘) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
296295ancoms 460 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
297 nn0uz 12810 . . . . . . . . . . . . . . . . . 18 β„•0 = (β„€β‰₯β€˜0)
2986, 297eleqtrdi 2844 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜0))
299 uzsplit 13519 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (β„€β‰₯β€˜0) β†’ (β„€β‰₯β€˜0) = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
300298, 299syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β„€β‰₯β€˜0) = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
301297, 300eqtrid 2785 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ β„•0 = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
302283uneq1d 4123 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
303301, 302eqtr2d 2774 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = β„•0)
304 ssequn1 4141 . . . . . . . . . . . . . . . . . 18 (β„š βŠ† β„‚ ↔ (β„š βˆͺ β„‚) = β„‚)
30593, 304mpbi 229 . . . . . . . . . . . . . . . . 17 (β„š βˆͺ β„‚) = β„‚
306305a1i 11 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β„š βˆͺ β„‚) = β„‚)
307303, 306feq23d 6664 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚) ↔ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚))
308307adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚) ↔ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚))
309296, 308mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚)
310 ffn 6669 . . . . . . . . . . . . . . . 16 (𝑀:(0...𝑁)βŸΆβ„š β†’ 𝑀 Fn (0...𝑁))
311 fnimadisj 6634 . . . . . . . . . . . . . . . 16 ((𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
312310, 286, 311syl2anr 598 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
3132nn0zd 12530 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 ∈ β„€)
314313peano2zd 12615 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ β„€)
315 uzid 12783 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ β„€ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)))
316 ne0i 4295 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)) β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
317314, 315, 3163syl 18 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
318 inidm 4179 . . . . . . . . . . . . . . . . . . 19 ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = (β„€β‰₯β€˜(𝑁 + 1))
319318neeq1i 3005 . . . . . . . . . . . . . . . . . 18 (((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ… ↔ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
320317, 319sylibr 233 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ…)
321 xpima2 6137 . . . . . . . . . . . . . . . . 17 (((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ… β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
322320, 321syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
323322adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
324312, 323uneq12d 4125 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1)))) = (βˆ… βˆͺ {0}))
325 imaundir 6104 . . . . . . . . . . . . . 14 ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))))
326 uncom 4114 . . . . . . . . . . . . . . 15 (βˆ… βˆͺ {0}) = ({0} βˆͺ βˆ…)
327 un0 4351 . . . . . . . . . . . . . . 15 ({0} βˆͺ βˆ…) = {0}
328326, 327eqtr2i 2762 . . . . . . . . . . . . . 14 {0} = (βˆ… βˆͺ {0})
329324, 325, 3283eqtr4g 2798 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
330286, 310anim12ci 615 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…))
331 fnconstg 6731 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1)))
332128, 331ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1))
333 fvun1 6933 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 Fn (0...𝑁) ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1)) ∧ (((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ… ∧ π‘˜ ∈ (0...𝑁))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
334332, 333mp3an2 1450 . . . . . . . . . . . . . . . . . . 19 ((𝑀 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ… ∧ π‘˜ ∈ (0...𝑁))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
335334anassrs 469 . . . . . . . . . . . . . . . . . 18 (((𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
336330, 335sylan 581 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
337336eqcomd 2739 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) = ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜))
338337oveq1d 7373 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = (((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
339338sumeq2dv 15593 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
340339mpteq2dv 5208 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜))))
341277, 276, 309, 329, 340coeeq 25604 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})))
342341reseq1d 5937 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)))
343 res0 5942 . . . . . . . . . . . . . 14 (𝑀 β†Ύ βˆ…) = βˆ…
344285reseq2d 5938 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑀 β†Ύ βˆ…) = (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
345 res0 5942 . . . . . . . . . . . . . . 15 (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ βˆ…) = βˆ…
346285reseq2d 5938 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ βˆ…) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
347345, 346eqtr3id 2787 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ… = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
348343, 344, 3473eqtr3a 2797 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
349 fss 6686 . . . . . . . . . . . . . . 15 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„š) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š)
350287, 289, 349mp2an 691 . . . . . . . . . . . . . 14 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š
351 fresaunres1 6716 . . . . . . . . . . . . . 14 ((𝑀:(0...𝑁)βŸΆβ„š ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š ∧ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
352350, 351mp3an2 1450 . . . . . . . . . . . . 13 ((𝑀:(0...𝑁)βŸΆβ„š ∧ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
353348, 352sylan2 594 . . . . . . . . . . . 12 ((𝑀:(0...𝑁)βŸΆβ„š ∧ πœ‘) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
354353ancoms 460 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
355342, 354eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀)
356 fveq2 6843 . . . . . . . . . . 11 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (coeffβ€˜0𝑝))
357356reseq1d 5937 . . . . . . . . . 10 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)))
358 eqtr2 2757 . . . . . . . . . . . 12 ((((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 ∧ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁))) β†’ 𝑀 = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)))
359 coe0 25633 . . . . . . . . . . . . . 14 (coeffβ€˜0𝑝) = (β„•0 Γ— {0})
360359reseq1i 5934 . . . . . . . . . . . . 13 ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) = ((β„•0 Γ— {0}) β†Ύ (0...𝑁))
361 elfznn0 13540 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (0...𝑁) β†’ π‘₯ ∈ β„•0)
362361ssriv 3949 . . . . . . . . . . . . . 14 (0...𝑁) βŠ† β„•0
363 xpssres 5975 . . . . . . . . . . . . . 14 ((0...𝑁) βŠ† β„•0 β†’ ((β„•0 Γ— {0}) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0}))
364362, 363ax-mp 5 . . . . . . . . . . . . 13 ((β„•0 Γ— {0}) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0})
365360, 364eqtri 2761 . . . . . . . . . . . 12 ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0})
366358, 365eqtrdi 2789 . . . . . . . . . . 11 ((((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 ∧ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁))) β†’ 𝑀 = ((0...𝑁) Γ— {0}))
367366ex 414 . . . . . . . . . 10 (((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 β†’ (((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) β†’ 𝑀 = ((0...𝑁) Γ— {0})))
368355, 357, 367syl2im 40 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ 𝑀 = ((0...𝑁) Γ— {0})))
369368necon3d 2961 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β‰  ((0...𝑁) Γ— {0}) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝))
370369impr 456 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝)
371 eldifsn 4748 . . . . . . 7 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}) ↔ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š) ∧ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝))
372278, 370, 371sylanbrc 584 . . . . . 6 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}))
373372adantrr 716 . . . . 5 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}))
374 oveq1 7365 . . . . . . . . . . . 12 (𝑦 = 𝐴 β†’ (π‘¦β†‘π‘˜) = (π΄β†‘π‘˜))
375374oveq2d 7374 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
376375sumeq2sdv 15594 . . . . . . . . . 10 (𝑦 = 𝐴 β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
377 eqid 2733 . . . . . . . . . 10 (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
378 sumex 15578 . . . . . . . . . 10 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) ∈ V
379376, 377, 378fvmpt 6949 . . . . . . . . 9 (𝐴 ∈ β„‚ β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
3801, 379syl 17 . . . . . . . 8 (πœ‘ β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
381380adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
382107adantll 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
383 aacllem.2 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
384383adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
385110, 384mulcld 11180 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
386385adantllr 718 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
38751, 382, 386fsummulc2 15674 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
388 aacllem.4 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β†‘π‘˜) = Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋))
389388oveq2d 7374 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)))
390389adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)))
391382adantr 482 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
392110adantllr 718 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„‚)
393 simpll 766 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ πœ‘)
394393, 383sylan 581 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
395391, 392, 394mulassd 11183 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = ((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
396395sumeq2dv 15593 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
397387, 390, 3963eqtr4d 2783 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
398397sumeq2dv 15593 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
399107ad2ant2lr 747 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
400110anasss 468 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
401400adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
402399, 401mulcld 11180 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
403383ad2ant2rl 748 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝑋 ∈ β„‚)
404402, 403mulcld 11180 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) ∈ β„‚)
40543, 69, 404fsumcom 15665 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
406398, 405eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
407406adantrr 716 . . . . . . . . 9 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
408 nfv 1918 . . . . . . . . . . . 12 β„²π‘›πœ‘
409 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑛 𝑀:(0...𝑁)βŸΆβ„š
410 nfra1 3266 . . . . . . . . . . . . 13 β„²π‘›βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0
411409, 410nfan 1903 . . . . . . . . . . . 12 Ⅎ𝑛(𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
412408, 411nfan 1903 . . . . . . . . . . 11 Ⅎ𝑛(πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
413 rspa 3230 . . . . . . . . . . . . . . . 16 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
414413oveq1d 7373 . . . . . . . . . . . . . . 15 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
415414adantll 713 . . . . . . . . . . . . . 14 (((𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
416415adantll 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
417383adantlr 714 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
41892, 417, 113fsummulc1 15675 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
419418adantlrr 720 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
420383mul02d 11358 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (0 Β· 𝑋) = 0)
421420adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (0 Β· 𝑋) = 0)
422416, 419, 4213eqtr3d 2781 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0)
423422ex 414 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ (𝑛 ∈ (1...𝑁) β†’ Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0))
424412, 423ralrimi 3239 . . . . . . . . . 10 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0)
425424sumeq2d 15592 . . . . . . . . 9 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426407, 425eqtrd 2773 . . . . . . . 8 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)0)
42722olci 865 . . . . . . . . 9 ((1...𝑁) βŠ† (β„€β‰₯β€˜π΅) ∨ (1...𝑁) ∈ Fin)
428 sumz 15612 . . . . . . . . 9 (((1...𝑁) βŠ† (β„€β‰₯β€˜π΅) ∨ (1...𝑁) ∈ Fin) β†’ Σ𝑛 ∈ (1...𝑁)0 = 0)
429427, 428ax-mp 5 . . . . . . . 8 Σ𝑛 ∈ (1...𝑁)0 = 0
430426, 429eqtrdi 2789 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = 0)
431381, 430eqtrd 2773 . . . . . 6 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0)
432431adantrlr 722 . . . . 5 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0)
433 fveq1 6842 . . . . . . 7 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ (π‘₯β€˜π΄) = ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄))
434433eqeq1d 2735 . . . . . 6 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ ((π‘₯β€˜π΄) = 0 ↔ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0))
435434rspcev 3580 . . . . 5 (((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}) ∧ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
436373, 432, 435syl2anc 585 . . . 4 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
437274, 436sylanr1 681 . . 3 ((πœ‘ ∧ (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
438271, 437rexlimddv 3155 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
439 elqaa 25698 . 2 (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ β„‚ ∧ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0))
4401, 438, 439sylanbrc 584 1 (πœ‘ β†’ 𝐴 ∈ 𝔸)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940   βˆ‰ wnel 3046  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3444   βˆ– cdif 3908   βˆͺ cun 3909   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587   class class class wbr 5106   ↦ cmpt 5189   Γ— cxp 5632  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   β€œ cima 5637   Fn wfn 6492  βŸΆwf 6493  β€“1-1β†’wf1 6494  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  (class class class)co 7358   ∘f cof 7616   ↑m cmap 8768   β‰ˆ cen 8883   β‰Ό cdom 8884  Fincfn 8886  β„‚cc 11054  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„šcq 12878  ...cfz 13430  β†‘cexp 13973  β™―chash 14236  Ξ£csu 15576  Basecbs 17088   β†Ύs cress 17117  .rcmulr 17139  Scalarcsca 17141   ·𝑠 cvsca 17142  0gc0g 17326   Ξ£g cgsu 17327  Moorecmre 17467  mrClscmrc 17468  mrIndcmri 17469  ACScacs 17470  Ringcrg 19969  DivRingcdr 20197  LModclmod 20336  LSubSpclss 20407  LSpanclspn 20447  LBasisclbs 20550  LVecclvec 20578  NzRingcnzr 20743  β„‚fldccnfld 20812   freeLMod cfrlm 21168   unitVec cuvc 21204   LIndF clindf 21226  LIndSclinds 21227  0𝑝c0p 25049  Polycply 25561  coeffccoe 25563  π”Έcaa 25690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-tpos 8158  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-oadd 8417  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-sup 9383  df-inf 9384  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-xnn0 12491  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-clim 15376  df-rlim 15377  df-sum 15577  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-0g 17328  df-gsum 17329  df-prds 17334  df-pws 17336  df-mre 17471  df-mrc 17472  df-mri 17473  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-mhm 18606  df-submnd 18607  df-grp 18756  df-minusg 18757  df-sbg 18758  df-mulg 18878  df-subg 18930  df-ghm 19011  df-cntz 19102  df-cmn 19569  df-abl 19570  df-mgp 19902  df-ur 19919  df-ring 19971  df-cring 19972  df-oppr 20054  df-dvdsr 20075  df-unit 20076  df-invr 20106  df-dvr 20117  df-drng 20199  df-subrg 20234  df-lmod 20338  df-lss 20408  df-lsp 20448  df-lmhm 20498  df-lbs 20551  df-lvec 20579  df-sra 20649  df-rgmod 20650  df-nzr 20744  df-cnfld 20813  df-dsmm 21154  df-frlm 21169  df-uvc 21205  df-lindf 21228  df-linds 21229  df-0p 25050  df-ply 25565  df-coe 25567  df-dgr 25568  df-aa 25691
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator