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 47896
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 12533 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ)
43ltp1d 12144 . . . . 5 (πœ‘ β†’ 𝑁 < (𝑁 + 1))
5 peano2nn0 12512 . . . . . . . 8 (𝑁 ∈ β„•0 β†’ (𝑁 + 1) ∈ β„•0)
62, 5syl 17 . . . . . . 7 (πœ‘ β†’ (𝑁 + 1) ∈ β„•0)
76nn0red 12533 . . . . . 6 (πœ‘ β†’ (𝑁 + 1) ∈ ℝ)
83, 7ltnled 11361 . . . . 5 (πœ‘ β†’ (𝑁 < (𝑁 + 1) ↔ Β¬ (𝑁 + 1) ≀ 𝑁))
94, 8mpbid 231 . . . 4 (πœ‘ β†’ Β¬ (𝑁 + 1) ≀ 𝑁)
10 aacllem.3 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
11103expa 1119 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
1211fmpttd 7115 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
13 qex 12945 . . . . . . . . . . 11 β„š ∈ V
14 ovex 7442 . . . . . . . . . . 11 (1...𝑁) ∈ V
1513, 14elmap 8865 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
1612, 15sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
1716fmpttd 7115 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)⟢(β„š ↑m (1...𝑁)))
18 eqid 2733 . . . . . . . . . . . 12 (β„‚fld β†Ύs β„š) = (β„‚fld β†Ύs β„š)
1918qdrng 27123 . . . . . . . . . . 11 (β„‚fld β†Ύs β„š) ∈ DivRing
20 drngring 20364 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ Ring)
2119, 20ax-mp 5 . . . . . . . . . 10 (β„‚fld β†Ύs β„š) ∈ Ring
22 fzfi 13937 . . . . . . . . . 10 (1...𝑁) ∈ Fin
23 eqid 2733 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) = ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))
2423frlmlmod 21304 . . . . . . . . . 10 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod)
2521, 22, 24mp2an 691 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod
26 fzfi 13937 . . . . . . . . 9 (0...𝑁) ∈ Fin
2718qrngbas 27122 . . . . . . . . . . . 12 β„š = (Baseβ€˜(β„‚fld β†Ύs β„š))
2823, 27frlmfibas 21317 . . . . . . . . . . 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 21308 . . . . . . . . . . 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 27124 . . . . . . . . . . . 12 0 = (0gβ€˜(β„‚fld β†Ύs β„š))
3423, 33frlm0 21309 . . . . . . . . . . 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 21317 . . . . . . . . . . 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 21393 . . . . . . . . 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 8843 . . . . . . . . 9 (𝑀 ∈ (β„š ↑m (0...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
43 fzfid 13938 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (0...𝑁) ∈ Fin)
44 fvexd 6907 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
4514mptex 7225 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V
4645a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V)
47 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
4847feqmptd 6961 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀 = (π‘˜ ∈ (0...𝑁) ↦ (π‘€β€˜π‘˜)))
49 eqidd 2734 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
5043, 44, 46, 48, 49offval2 7690 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢))))
51 fzfid 13938 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (1...𝑁) ∈ Fin)
52 ffvelcdm 7084 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5352adantll 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5416adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
55 cnfldmul 20950 . . . . . . . . . . . . . . . . . . . . . 22 Β· = (.rβ€˜β„‚fld)
5618, 55ressmulr 17252 . . . . . . . . . . . . . . . . . . . . 21 (β„š ∈ V β†’ Β· = (.rβ€˜(β„‚fld β†Ύs β„š)))
5713, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Β· = (.rβ€˜(β„‚fld β†Ύs β„š))
5823, 29, 27, 51, 53, 54, 32, 57frlmvscafval 21321 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
59 fvexd 6907 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
6011adantllr 718 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
61 fconstmpt 5739 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜))
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜)))
63 eqidd 2734 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) = (𝑛 ∈ (1...𝑁) ↦ 𝐢))
6451, 59, 60, 62, 63offval2 7690 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6558, 64eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6665mpteq2dva 5249 . . . . . . . . . . . . . . . . 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 7425 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
69 fzfid 13938 . . . . . . . . . . . . . . . 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 12951 . . . . . . . . . . . . . . . . . . . 20 (((π‘€β€˜π‘˜) ∈ β„š ∧ 𝐢 ∈ β„š) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7571, 73, 74syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7675an32s 651 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7776fmpttd 7115 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7813, 14elmap 8865 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7977, 78sylibr 233 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)))
80 eqid 2733 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
8114mptex 7225 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V)
83 snex 5432 . . . . . . . . . . . . . . . . . . 19 {0} ∈ V
8414, 83xpex 7740 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) Γ— {0}) ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((1...𝑁) Γ— {0}) ∈ V)
8680, 43, 82, 85fsuppmptdm 9374 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) finSupp ((1...𝑁) Γ— {0}))
8723, 29, 35, 69, 43, 70, 79, 86frlmgsum 21327 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
88 cnfldbas 20948 . . . . . . . . . . . . . . . . . 18 β„‚ = (Baseβ€˜β„‚fld)
89 cnfldadd 20949 . . . . . . . . . . . . . . . . . 18 + = (+gβ€˜β„‚fld)
90 cnfldex 20947 . . . . . . . . . . . . . . . . . . 19 β„‚fld ∈ V
9190a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„‚fld ∈ V)
92 fzfid 13938 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (0...𝑁) ∈ Fin)
93 qsscn 12944 . . . . . . . . . . . . . . . . . . 19 β„š βŠ† β„‚
9493a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„š βŠ† β„‚)
9575fmpttd 7115 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(0...𝑁)βŸΆβ„š)
96 0z 12569 . . . . . . . . . . . . . . . . . . . 20 0 ∈ β„€
97 zq 12938 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„€ β†’ 0 ∈ β„š)
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . 19 0 ∈ β„š
9998a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 0 ∈ β„š)
100 addlid 11397 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (0 + π‘₯) = π‘₯)
101 addrid 11394 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (π‘₯ + 0) = π‘₯)
102100, 101jca 513 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ β„‚ β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
103102adantl 483 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ β„‚) β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
10488, 89, 18, 91, 92, 94, 95, 99, 103gsumress 18601 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
105 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
106 qcn 12947 . . . . . . . . . . . . . . . . . . . . 21 ((π‘€β€˜π‘˜) ∈ β„š β†’ (π‘€β€˜π‘˜) ∈ β„‚)
10752, 106syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
108105, 107sylan 581 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
109 qcn 12947 . . . . . . . . . . . . . . . . . . . . . 22 (𝐢 ∈ β„š β†’ 𝐢 ∈ β„‚)
11011, 109syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„‚)
111110an32s 651 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
112111adantllr 718 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
113108, 112mulcld 11234 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
11492, 113gsumfsum 21012 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
115104, 114eqtr3d 2775 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
116115mpteq2dva 5249 . . . . . . . . . . . . . . 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 12949 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š) β†’ (π‘₯ + 𝑦) ∈ β„š)
119118adantl 483 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ (π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š)) β†’ (π‘₯ + 𝑦) ∈ β„š)
12094, 119, 92, 75, 99fsumcllem 15678 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
121120fmpttd 7115 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
12213, 14elmap 8865 . . . . . . . . . . . . . . 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 8843 . . . . . . . . . . . . 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 6718 . . . . . . . . . . . . 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 11208 . . . . . . . . . . . . 13 0 ∈ V
129 fnconstg 6780 . . . . . . . . . . . . 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 5257 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐢)
137135, 136nfmpt 5256 . . . . . . . . . . . . . . 15 Ⅎ𝑛(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
138133, 134, 137nfov 7439 . . . . . . . . . . . . . 14 Ⅎ𝑛(𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
139131, 132, 138nfov 7439 . . . . . . . . . . . . 13 Ⅎ𝑛(((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))
140 nfcv 2904 . . . . . . . . . . . . 13 Ⅎ𝑛((1...𝑁) Γ— {0})
141139, 140eqfnfv2f 7037 . . . . . . . . . . . 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 6894 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›))
144 sumex 15634 . . . . . . . . . . . . . . 15 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ V
145 eqid 2733 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
146145fvmpt2 7010 . . . . . . . . . . . . . . 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 7205 . . . . . . . . . . . . . 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 3176 . . . . . . . . . . 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 3176 . . . . . . 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 20377 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ NzRing)
15919, 158ax-mp 5 . . . . . . . 8 (β„‚fld β†Ύs β„š) ∈ NzRing
16031islindf3 21381 . . . . . . . 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 6695 . . . . . . . . 9 dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (0...𝑁)
164 f1eq2 6784 . . . . . . . . 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 3048 . . . . . . . . . . 11 (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} ↔ Β¬ 𝑀 ∈ {((0...𝑁) Γ— {0})})
170 velsn 4645 . . . . . . . . . . 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 3094 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
175 raldifb 4145 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ↔ βˆ€π‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
176 ralnex 3073 . . . . . . 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 20577 . . . . . . . . . . . 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 20600 . . . . . . . . . . 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 20715 . . . . . . . . . . . . 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 20757 . . . . . . . . . . . . 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 6726 . . . . . . . . . . . 12 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† (β„š ↑m (1...𝑁)))
195 dif0 4373 . . . . . . . . . . . 12 ((β„š ↑m (1...𝑁)) βˆ– βˆ…) = (β„š ↑m (1...𝑁))
196194, 195sseqtrrdi 4034 . . . . . . . . . . 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 21346 . . . . . . . . . . . . . 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 6725 . . . . . . . . . . . . 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 4020 . . . . . . . . . . 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 4391 . . . . . . . . . . . . . 14 (ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…) = ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
206205fveq2i 6895 . . . . . . . . . . . . 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 21352 . . . . . . . . . . . . . . 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 20690 . . . . . . . . . . . . . 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 4034 . . . . . . . . . . 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 4391 . . . . . . . . . . 11 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆͺ βˆ…) = ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
21625, 159pm3.2i 472 . . . . . . . . . . . . . 14 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ NzRing)
217183, 31lindsind2 21374 . . . . . . . . . . . . . 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 3147 . . . . . . . . . . . 12 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) β†’ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
220186, 187ismri2 17576 . . . . . . . . . . . . . 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 9351 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin)
226 rnfi 9335 . . . . . . . . . . . . 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 17592 . . . . . . . . 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 7442 . . . . . . . . . . . . 13 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
233232rnex 7903 . . . . . . . . . . . 12 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
234 elpwi 4610 . . . . . . . . . . . 12 (𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ 𝑣 βŠ† ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
235 ssdomg 8996 . . . . . . . . . . . 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 9008 . . . . . . . . . . . . . 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 6845 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1-ontoβ†’ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
240 ovex 7442 . . . . . . . . . . . . . . . . 17 (0...𝑁) ∈ V
241240f1oen 8969 . . . . . . . . . . . . . . . 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 9008 . . . . . . . . . . . . . . . . 17 (((0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
244198uvcendim 21402 . . . . . . . . . . . . . . . . . . . 20 (((β„‚fld β†Ύs β„š) ∈ NzRing ∧ (1...𝑁) ∈ Fin) β†’ (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
245159, 22, 244mp2an 691 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
246245ensymi 9000 . . . . . . . . . . . . . . . . . 18 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)
247 domentr 9009 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)) β†’ (0...𝑁) β‰Ό (1...𝑁))
248 hashdom 14339 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) β†’ ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁)))
24926, 22, 248mp2an 691 . . . . . . . . . . . . . . . . . . . 20 ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁))
250 hashfz0 14392 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
2512, 250syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
252 hashfz1 14306 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(1...𝑁)) = 𝑁)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(1...𝑁)) = 𝑁)
254251, 253breq12d 5162 . . . . . . . . . . . . . . . . . . . 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 3156 . . . . . . . 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 4791 . . . . 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 25716 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
278277adantrr 716 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
279 uzdisj 13574 . . . . . . . . . . . . . . . . . 18 ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…
2802nn0cnd 12534 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ β„‚)
281 pncan1 11638 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„‚ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
283282oveq2d 7425 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (0...((𝑁 + 1) βˆ’ 1)) = (0...𝑁))
284283ineq1d 4212 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
285279, 284eqtr3id 2787 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ… = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
286285eqcomd 2739 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
287128fconst 6778 . . . . . . . . . . . . . . . . . 18 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0}
288 snssi 4812 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„š β†’ {0} βŠ† β„š)
28996, 97, 288mp2b 10 . . . . . . . . . . . . . . . . . . 19 {0} βŠ† β„š
290289, 93sstri 3992 . . . . . . . . . . . . . . . . . 18 {0} βŠ† β„‚
291 fss 6735 . . . . . . . . . . . . . . . . . 18 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„‚) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚)
292287, 290, 291mp2an 691 . . . . . . . . . . . . . . . . 17 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚
293 fun 6754 . . . . . . . . . . . . . . . . 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 12864 . . . . . . . . . . . . . . . . . 18 β„•0 = (β„€β‰₯β€˜0)
2986, 297eleqtrdi 2844 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜0))
299 uzsplit 13573 . . . . . . . . . . . . . . . . . . 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 4163 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
303301, 302eqtr2d 2774 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = β„•0)
304 ssequn1 4181 . . . . . . . . . . . . . . . . . 18 (β„š βŠ† β„‚ ↔ (β„š βˆͺ β„‚) = β„‚)
30593, 304mpbi 229 . . . . . . . . . . . . . . . . 17 (β„š βˆͺ β„‚) = β„‚
306305a1i 11 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β„š βˆͺ β„‚) = β„‚)
307303, 306feq23d 6713 . . . . . . . . . . . . . . 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 6718 . . . . . . . . . . . . . . . 16 (𝑀:(0...𝑁)βŸΆβ„š β†’ 𝑀 Fn (0...𝑁))
311 fnimadisj 6683 . . . . . . . . . . . . . . . 16 ((𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
312310, 286, 311syl2anr 598 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
3132nn0zd 12584 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 ∈ β„€)
314313peano2zd 12669 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ β„€)
315 uzid 12837 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ β„€ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)))
316 ne0i 4335 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)) β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
317314, 315, 3163syl 18 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
318 inidm 4219 . . . . . . . . . . . . . . . . . . 19 ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = (β„€β‰₯β€˜(𝑁 + 1))
319318neeq1i 3006 . . . . . . . . . . . . . . . . . 18 (((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ… ↔ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
320317, 319sylibr 233 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ…)
321 xpima2 6184 . . . . . . . . . . . . . . . . 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 4165 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1)))) = (βˆ… βˆͺ {0}))
325 imaundir 6151 . . . . . . . . . . . . . 14 ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))))
326 uncom 4154 . . . . . . . . . . . . . . 15 (βˆ… βˆͺ {0}) = ({0} βˆͺ βˆ…)
327 un0 4391 . . . . . . . . . . . . . . 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 6780 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1)))
332128, 331ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1))
333 fvun1 6983 . . . . . . . . . . . . . . . . . . . 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 7424 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = (((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
339338sumeq2dv 15649 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
340339mpteq2dv 5251 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜))))
341277, 276, 309, 329, 340coeeq 25741 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})))
342341reseq1d 5981 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)))
343 res0 5986 . . . . . . . . . . . . . 14 (𝑀 β†Ύ βˆ…) = βˆ…
344285reseq2d 5982 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑀 β†Ύ βˆ…) = (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
345 res0 5986 . . . . . . . . . . . . . . 15 (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ βˆ…) = βˆ…
346285reseq2d 5982 . . . . . . . . . . . . . . 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 6735 . . . . . . . . . . . . . . 15 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„š) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š)
350287, 289, 349mp2an 691 . . . . . . . . . . . . . 14 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š
351 fresaunres1 6765 . . . . . . . . . . . . . 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 6892 . . . . . . . . . . 11 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (coeffβ€˜0𝑝))
357356reseq1d 5981 . . . . . . . . . 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 25770 . . . . . . . . . . . . . 14 (coeffβ€˜0𝑝) = (β„•0 Γ— {0})
360359reseq1i 5978 . . . . . . . . . . . . 13 ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) = ((β„•0 Γ— {0}) β†Ύ (0...𝑁))
361 elfznn0 13594 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (0...𝑁) β†’ π‘₯ ∈ β„•0)
362361ssriv 3987 . . . . . . . . . . . . . 14 (0...𝑁) βŠ† β„•0
363 xpssres 6019 . . . . . . . . . . . . . 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 2962 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β‰  ((0...𝑁) Γ— {0}) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝))
370369impr 456 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝)
371 eldifsn 4791 . . . . . . 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 7416 . . . . . . . . . . . 12 (𝑦 = 𝐴 β†’ (π‘¦β†‘π‘˜) = (π΄β†‘π‘˜))
375374oveq2d 7425 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
376375sumeq2sdv 15650 . . . . . . . . . 10 (𝑦 = 𝐴 β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
377 eqid 2733 . . . . . . . . . 10 (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
378 sumex 15634 . . . . . . . . . 10 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) ∈ V
379376, 377, 378fvmpt 6999 . . . . . . . . 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 11234 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
386385adantllr 718 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
38751, 382, 386fsummulc2 15730 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
388 aacllem.4 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β†‘π‘˜) = Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋))
389388oveq2d 7425 . . . . . . . . . . . . . 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 11237 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = ((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
396395sumeq2dv 15649 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
397387, 390, 3963eqtr4d 2783 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
398397sumeq2dv 15649 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
399107ad2ant2lr 747 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
400110anasss 468 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
401400adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
402399, 401mulcld 11234 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
403383ad2ant2rl 748 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝑋 ∈ β„‚)
404402, 403mulcld 11234 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) ∈ β„‚)
40543, 69, 404fsumcom 15721 . . . . . . . . . . 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 3282 . . . . . . . . . . . . 13 β„²π‘›βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0
411409, 410nfan 1903 . . . . . . . . . . . 12 Ⅎ𝑛(𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
412408, 411nfan 1903 . . . . . . . . . . 11 Ⅎ𝑛(πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
413 rspa 3246 . . . . . . . . . . . . . . . 16 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
414413oveq1d 7424 . . . . . . . . . . . . . . 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 15731 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
419418adantlrr 720 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
420383mul02d 11412 . . . . . . . . . . . . . 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 3255 . . . . . . . . . 10 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0)
425424sumeq2d 15648 . . . . . . . . 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 15668 . . . . . . . . 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 6891 . . . . . . 7 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ (π‘₯β€˜π΄) = ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄))
434433eqeq1d 2735 . . . . . 6 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ ((π‘₯β€˜π΄) = 0 ↔ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0))
435434rspcev 3613 . . . . 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 3162 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
439 elqaa 25835 . 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 2941   βˆ‰ wnel 3047  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629   class class class wbr 5149   ↦ cmpt 5232   Γ— cxp 5675  dom cdm 5677  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680   Fn wfn 6539  βŸΆwf 6540  β€“1-1β†’wf1 6541  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409   ∘f cof 7668   ↑m cmap 8820   β‰ˆ cen 8936   β‰Ό cdom 8937  Fincfn 8939  β„‚cc 11108  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444  β„•0cn0 12472  β„€cz 12558  β„€β‰₯cuz 12822  β„šcq 12932  ...cfz 13484  β†‘cexp 14027  β™―chash 14290  Ξ£csu 15632  Basecbs 17144   β†Ύs cress 17173  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  0gc0g 17385   Ξ£g cgsu 17386  Moorecmre 17526  mrClscmrc 17527  mrIndcmri 17528  ACScacs 17529  Ringcrg 20056  NzRingcnzr 20291  DivRingcdr 20357  LModclmod 20471  LSubSpclss 20542  LSpanclspn 20582  LBasisclbs 20685  LVecclvec 20713  β„‚fldccnfld 20944   freeLMod cfrlm 21301   unitVec cuvc 21337   LIndF clindf 21359  LIndSclinds 21360  0𝑝c0p 25186  Polycply 25698  coeffccoe 25700  π”Έcaa 25827
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189  ax-mulf 11190
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-tpos 8211  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-xnn0 12545  df-z 12559  df-dec 12678  df-uz 12823  df-q 12933  df-rp 12975  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-rlim 15433  df-sum 15633  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-starv 17212  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-unif 17220  df-hom 17221  df-cco 17222  df-0g 17387  df-gsum 17388  df-prds 17393  df-pws 17395  df-mre 17530  df-mrc 17531  df-mri 17532  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-mhm 18671  df-submnd 18672  df-grp 18822  df-minusg 18823  df-sbg 18824  df-mulg 18951  df-subg 19003  df-ghm 19090  df-cntz 19181  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-cring 20059  df-oppr 20150  df-dvdsr 20171  df-unit 20172  df-invr 20202  df-dvr 20215  df-nzr 20292  df-subrg 20317  df-drng 20359  df-lmod 20473  df-lss 20543  df-lsp 20583  df-lmhm 20633  df-lbs 20686  df-lvec 20714  df-sra 20785  df-rgmod 20786  df-cnfld 20945  df-dsmm 21287  df-frlm 21302  df-uvc 21338  df-lindf 21361  df-linds 21362  df-0p 25187  df-ply 25702  df-coe 25704  df-dgr 25705  df-aa 25828
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator