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 47936
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 12538 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ)
43ltp1d 12149 . . . . 5 (πœ‘ β†’ 𝑁 < (𝑁 + 1))
5 peano2nn0 12517 . . . . . . . 8 (𝑁 ∈ β„•0 β†’ (𝑁 + 1) ∈ β„•0)
62, 5syl 17 . . . . . . 7 (πœ‘ β†’ (𝑁 + 1) ∈ β„•0)
76nn0red 12538 . . . . . 6 (πœ‘ β†’ (𝑁 + 1) ∈ ℝ)
83, 7ltnled 11366 . . . . 5 (πœ‘ β†’ (𝑁 < (𝑁 + 1) ↔ Β¬ (𝑁 + 1) ≀ 𝑁))
94, 8mpbid 231 . . . 4 (πœ‘ β†’ Β¬ (𝑁 + 1) ≀ 𝑁)
10 aacllem.3 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
11103expa 1117 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
1211fmpttd 7116 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
13 qex 12950 . . . . . . . . . . 11 β„š ∈ V
14 ovex 7445 . . . . . . . . . . 11 (1...𝑁) ∈ V
1513, 14elmap 8868 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
1612, 15sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
1716fmpttd 7116 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)⟢(β„š ↑m (1...𝑁)))
18 eqid 2731 . . . . . . . . . . . 12 (β„‚fld β†Ύs β„š) = (β„‚fld β†Ύs β„š)
1918qdrng 27360 . . . . . . . . . . 11 (β„‚fld β†Ύs β„š) ∈ DivRing
20 drngring 20508 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ Ring)
2119, 20ax-mp 5 . . . . . . . . . 10 (β„‚fld β†Ύs β„š) ∈ Ring
22 fzfi 13942 . . . . . . . . . 10 (1...𝑁) ∈ Fin
23 eqid 2731 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) = ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))
2423frlmlmod 21524 . . . . . . . . . 10 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod)
2521, 22, 24mp2an 689 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod
26 fzfi 13942 . . . . . . . . 9 (0...𝑁) ∈ Fin
2718qrngbas 27359 . . . . . . . . . . . 12 β„š = (Baseβ€˜(β„‚fld β†Ύs β„š))
2823, 27frlmfibas 21537 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (1...𝑁) ∈ Fin) β†’ (β„š ↑m (1...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
2919, 22, 28mp2an 689 . . . . . . . . . 10 (β„š ↑m (1...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
3023frlmsca 21528 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (1...𝑁) ∈ Fin) β†’ (β„‚fld β†Ύs β„š) = (Scalarβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
3119, 22, 30mp2an 689 . . . . . . . . . 10 (β„‚fld β†Ύs β„š) = (Scalarβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
32 eqid 2731 . . . . . . . . . 10 ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
3318qrng0 27361 . . . . . . . . . . . 12 0 = (0gβ€˜(β„‚fld β†Ύs β„š))
3423, 33frlm0 21529 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((1...𝑁) Γ— {0}) = (0gβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
3521, 22, 34mp2an 689 . . . . . . . . . 10 ((1...𝑁) Γ— {0}) = (0gβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
36 eqid 2731 . . . . . . . . . . . 12 ((β„‚fld β†Ύs β„š) freeLMod (0...𝑁)) = ((β„‚fld β†Ύs β„š) freeLMod (0...𝑁))
3736, 27frlmfibas 21537 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (0...𝑁) ∈ Fin) β†’ (β„š ↑m (0...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (0...𝑁))))
3819, 26, 37mp2an 689 . . . . . . . . . 10 (β„š ↑m (0...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (0...𝑁)))
3929, 31, 32, 35, 33, 38islindf4 21613 . . . . . . . . 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 1450 . . . . . . . 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 8846 . . . . . . . . 9 (𝑀 ∈ (β„š ↑m (0...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
43 fzfid 13943 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (0...𝑁) ∈ Fin)
44 fvexd 6906 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
4514mptex 7227 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V
4645a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V)
47 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
4847feqmptd 6960 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀 = (π‘˜ ∈ (0...𝑁) ↦ (π‘€β€˜π‘˜)))
49 eqidd 2732 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
5043, 44, 46, 48, 49offval2 7693 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢))))
51 fzfid 13943 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (1...𝑁) ∈ Fin)
52 ffvelcdm 7083 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5352adantll 711 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5416adantlr 712 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
55 cnfldmul 21151 . . . . . . . . . . . . . . . . . . . . . 22 Β· = (.rβ€˜β„‚fld)
5618, 55ressmulr 17257 . . . . . . . . . . . . . . . . . . . . 21 (β„š ∈ V β†’ Β· = (.rβ€˜(β„‚fld β†Ύs β„š)))
5713, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Β· = (.rβ€˜(β„‚fld β†Ύs β„š))
5823, 29, 27, 51, 53, 54, 32, 57frlmvscafval 21541 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
59 fvexd 6906 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
6011adantllr 716 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
61 fconstmpt 5738 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜))
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜)))
63 eqidd 2732 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) = (𝑛 ∈ (1...𝑁) ↦ 𝐢))
6451, 59, 60, 62, 63offval2 7693 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6558, 64eqtrd 2771 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6665mpteq2dva 5248 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
6750, 66eqtrd 2771 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
6867oveq2d 7428 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
69 fzfid 13943 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (1...𝑁) ∈ Fin)
7021a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (β„‚fld β†Ύs β„š) ∈ Ring)
7153adantlr 712 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
7211an32s 649 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„š)
7372adantllr 716 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„š)
74 qmulcl 12956 . . . . . . . . . . . . . . . . . . . 20 (((π‘€β€˜π‘˜) ∈ β„š ∧ 𝐢 ∈ β„š) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7571, 73, 74syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7675an32s 649 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7776fmpttd 7116 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7813, 14elmap 8868 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7977, 78sylibr 233 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)))
80 eqid 2731 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
8114mptex 7227 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V)
83 snex 5431 . . . . . . . . . . . . . . . . . . 19 {0} ∈ V
8414, 83xpex 7743 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) Γ— {0}) ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((1...𝑁) Γ— {0}) ∈ V)
8680, 43, 82, 85fsuppmptdm 9377 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) finSupp ((1...𝑁) Γ— {0}))
8723, 29, 35, 69, 43, 70, 79, 86frlmgsum 21547 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
88 cnfldbas 21149 . . . . . . . . . . . . . . . . . 18 β„‚ = (Baseβ€˜β„‚fld)
89 cnfldadd 21150 . . . . . . . . . . . . . . . . . 18 + = (+gβ€˜β„‚fld)
90 cnfldex 21148 . . . . . . . . . . . . . . . . . . 19 β„‚fld ∈ V
9190a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„‚fld ∈ V)
92 fzfid 13943 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (0...𝑁) ∈ Fin)
93 qsscn 12949 . . . . . . . . . . . . . . . . . . 19 β„š βŠ† β„‚
9493a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„š βŠ† β„‚)
9575fmpttd 7116 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(0...𝑁)βŸΆβ„š)
96 0z 12574 . . . . . . . . . . . . . . . . . . . 20 0 ∈ β„€
97 zq 12943 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„€ β†’ 0 ∈ β„š)
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . 19 0 ∈ β„š
9998a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 0 ∈ β„š)
100 addlid 11402 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (0 + π‘₯) = π‘₯)
101 addrid 11399 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (π‘₯ + 0) = π‘₯)
102100, 101jca 511 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ β„‚ β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
103102adantl 481 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ β„‚) β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
10488, 89, 18, 91, 92, 94, 95, 99, 103gsumress 18608 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
105 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
106 qcn 12952 . . . . . . . . . . . . . . . . . . . . 21 ((π‘€β€˜π‘˜) ∈ β„š β†’ (π‘€β€˜π‘˜) ∈ β„‚)
10752, 106syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
108105, 107sylan 579 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
109 qcn 12952 . . . . . . . . . . . . . . . . . . . . . 22 (𝐢 ∈ β„š β†’ 𝐢 ∈ β„‚)
11011, 109syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„‚)
111110an32s 649 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
112111adantllr 716 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
113108, 112mulcld 11239 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
11492, 113gsumfsum 21213 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
115104, 114eqtr3d 2773 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
116115mpteq2dva 5248 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)))
11768, 87, 1163eqtrd 2775 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)))
118 qaddcl 12954 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š) β†’ (π‘₯ + 𝑦) ∈ β„š)
119118adantl 481 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ (π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š)) β†’ (π‘₯ + 𝑦) ∈ β„š)
12094, 119, 92, 75, 99fsumcllem 15683 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
121120fmpttd 7116 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
12213, 14elmap 8868 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
123121, 122sylibr 233 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)))
124117, 123eqeltrd 2832 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) ∈ (β„š ↑m (1...𝑁)))
125 elmapi 8846 . . . . . . . . . . . . 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 6717 . . . . . . . . . . . . 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 11213 . . . . . . . . . . . . 13 0 ∈ V
129 fnconstg 6779 . . . . . . . . . . . . 13 (0 ∈ V β†’ ((1...𝑁) Γ— {0}) Fn (1...𝑁))
130128, 129ax-mp 5 . . . . . . . . . . . 12 ((1...𝑁) Γ— {0}) Fn (1...𝑁)
131 nfcv 2902 . . . . . . . . . . . . . 14 Ⅎ𝑛((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))
132 nfcv 2902 . . . . . . . . . . . . . 14 Ⅎ𝑛 Ξ£g
133 nfcv 2902 . . . . . . . . . . . . . . 15 Ⅎ𝑛𝑀
134 nfcv 2902 . . . . . . . . . . . . . . 15 Ⅎ𝑛 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
135 nfcv 2902 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(0...𝑁)
136 nfmpt1 5256 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐢)
137135, 136nfmpt 5255 . . . . . . . . . . . . . . 15 Ⅎ𝑛(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
138133, 134, 137nfov 7442 . . . . . . . . . . . . . 14 Ⅎ𝑛(𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
139131, 132, 138nfov 7442 . . . . . . . . . . . . 13 Ⅎ𝑛(((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))
140 nfcv 2902 . . . . . . . . . . . . 13 Ⅎ𝑛((1...𝑁) Γ— {0})
141139, 140eqfnfv2f 7036 . . . . . . . . . . . 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 585 . . . . . . . . . . 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 6893 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›))
144 sumex 15639 . . . . . . . . . . . . . . 15 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ V
145 eqid 2731 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
146145fvmpt2 7009 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ V) β†’ ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
147144, 146mpan2 688 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
148143, 147sylan9eq 2791 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
149128fvconst2 7207 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {0})β€˜π‘›) = 0)
150149adantl 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((1...𝑁) Γ— {0})β€˜π‘›) = 0)
151148, 150eqeq12d 2747 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = (((1...𝑁) Γ— {0})β€˜π‘›) ↔ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
152151ralbidva 3174 . . . . . . . . . . 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 341 . . . . . . . . 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 592 . . . . . . . 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 3174 . . . . . . 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 20521 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ NzRing)
15919, 158ax-mp 5 . . . . . . . 8 (β„‚fld β†Ύs β„š) ∈ NzRing
16031islindf3 21601 . . . . . . . 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 689 . . . . . . 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 2731 . . . . . . . . . 10 (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
16345, 162dmmpti 6694 . . . . . . . . 9 dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (0...𝑁)
164 f1eq2 6783 . . . . . . . . 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 623 . . . . . . 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 3046 . . . . . . . . . . 11 (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} ↔ Β¬ 𝑀 ∈ {((0...𝑁) Γ— {0})})
170 velsn 4644 . . . . . . . . . . 11 (𝑀 ∈ {((0...𝑁) Γ— {0})} ↔ 𝑀 = ((0...𝑁) Γ— {0}))
171169, 170xchbinx 334 . . . . . . . . . 10 (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} ↔ Β¬ 𝑀 = ((0...𝑁) Γ— {0}))
172171imbi1i 349 . . . . . . . . 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 3092 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
175 raldifb 4144 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ↔ βˆ€π‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
176 ralnex 3071 . . . . . . 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 2731 . . . . . . . . . . . . 13 (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
18029, 179lssmre 20722 . . . . . . . . . . . 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 2731 . . . . . . . . . . . 12 (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
184 eqid 2731 . . . . . . . . . . . 12 (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) = (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
185179, 183, 184mrclsp 20745 . . . . . . . . . . 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 2731 . . . . . . . . . 10 (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) = (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
18831islvec 20860 . . . . . . . . . . . . 13 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec ↔ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ DivRing))
18925, 19, 188mpbir2an 708 . . . . . . . . . . . 12 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec
190179, 186, 29lssacsex 20903 . . . . . . . . . . . . 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 495 . . . . . . . . . . . 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 6725 . . . . . . . . . . . 12 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† (β„š ↑m (1...𝑁)))
195 dif0 4372 . . . . . . . . . . . 12 ((β„š ↑m (1...𝑁)) βˆ– βˆ…) = (β„š ↑m (1...𝑁))
196194, 195sseqtrrdi 4033 . . . . . . . . . . 11 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…))
197196adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…))
198 eqid 2731 . . . . . . . . . . . . . . 15 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) = ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
199198, 23, 29uvcff 21566 . . . . . . . . . . . . . 14 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)):(1...𝑁)⟢(β„š ↑m (1...𝑁)))
20021, 22, 199mp2an 689 . . . . . . . . . . . . 13 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)):(1...𝑁)⟢(β„š ↑m (1...𝑁))
201 frn 6724 . . . . . . . . . . . . 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 4019 . . . . . . . . . . 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 4390 . . . . . . . . . . . . . 14 (ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…) = ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
206205fveq2i 6894 . . . . . . . . . . . . 13 ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)) = ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
207 eqid 2731 . . . . . . . . . . . . . . . 16 (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
20823, 198, 207frlmlbs 21572 . . . . . . . . . . . . . . 15 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
20921, 22, 208mp2an 689 . . . . . . . . . . . . . 14 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
21029, 207, 183lbssp 20835 . . . . . . . . . . . . . 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 2759 . . . . . . . . . . . 12 ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)) = (β„š ↑m (1...𝑁))
213194, 212sseqtrrdi 4033 . . . . . . . . . . 11 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)))
214213adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)))
215 un0 4390 . . . . . . . . . . 11 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆͺ βˆ…) = ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
21625, 159pm3.2i 470 . . . . . . . . . . . . . 14 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ NzRing)
217183, 31lindsind2 21594 . . . . . . . . . . . . . 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 1447 . . . . . . . . . . . . 13 ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∧ π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) β†’ Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
219218ralrimiva 3145 . . . . . . . . . . . 12 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) β†’ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
220186, 187ismri2 17581 . . . . . . . . . . . . . 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 586 . . . . . . . . . . . . 13 (πœ‘ β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) ↔ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯}))))
222221biimpar 477 . . . . . . . . . . . 12 ((πœ‘ ∧ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯}))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
223219, 222sylan2 592 . . . . . . . . . . 11 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
224215, 223eqeltrid 2836 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
225 mptfi 9354 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin)
226 rnfi 9338 . . . . . . . . . . . . 13 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin)
22726, 225, 226mp2b 10 . . . . . . . . . . . 12 ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin
228227orci 862 . . . . . . . . . . 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 17597 . . . . . . . . 9 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ βˆƒπ‘£ ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))))
231230ex 412 . . . . . . . 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 7445 . . . . . . . . . . . . 13 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
233232rnex 7906 . . . . . . . . . . . 12 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
234 elpwi 4609 . . . . . . . . . . . 12 (𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ 𝑣 βŠ† ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
235 ssdomg 8999 . . . . . . . . . . . 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 9011 . . . . . . . . . . . . . 14 ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
238237ancoms 458 . . . . . . . . . . . . 13 ((𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
239 f1f1orn 6844 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1-ontoβ†’ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
240 ovex 7445 . . . . . . . . . . . . . . . . 17 (0...𝑁) ∈ V
241240f1oen 8972 . . . . . . . . . . . . . . . 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 9011 . . . . . . . . . . . . . . . . 17 (((0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
244198uvcendim 21622 . . . . . . . . . . . . . . . . . . . 20 (((β„‚fld β†Ύs β„š) ∈ NzRing ∧ (1...𝑁) ∈ Fin) β†’ (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
245159, 22, 244mp2an 689 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
246245ensymi 9003 . . . . . . . . . . . . . . . . . 18 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)
247 domentr 9012 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)) β†’ (0...𝑁) β‰Ό (1...𝑁))
248 hashdom 14344 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) β†’ ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁)))
24926, 22, 248mp2an 689 . . . . . . . . . . . . . . . . . . . 20 ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁))
250 hashfz0 14397 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
2512, 250syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
252 hashfz1 14311 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(1...𝑁)) = 𝑁)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(1...𝑁)) = 𝑁)
254251, 253breq12d 5161 . . . . . . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . . . . . 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 415 . . . . . . . . . . . . . . 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 452 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
264236, 263sylan2 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
265264adantrd 491 . . . . . . . . 9 ((πœ‘ ∧ 𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
266265rexlimdva 3154 . . . . . . . 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 410 . . . . . 6 (πœ‘ β†’ ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∧ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V) β†’ (𝑁 + 1) ≀ 𝑁))
269268ancomsd 465 . . . . 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 4790 . . . . 5 (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) ↔ (𝑀 ∈ (β„š ↑m (0...𝑁)) ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
27342anim1i 614 . . . . 5 ((𝑀 ∈ (β„š ↑m (0...𝑁)) ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) β†’ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
274272, 273sylbi 216 . . . 4 (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) β†’ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
27593a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ β„š βŠ† β„‚)
2762adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑁 ∈ β„•0)
277275, 276, 53elplyd 25952 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
278277adantrr 714 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
279 uzdisj 13579 . . . . . . . . . . . . . . . . . 18 ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…
2802nn0cnd 12539 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ β„‚)
281 pncan1 11643 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„‚ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
283282oveq2d 7428 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (0...((𝑁 + 1) βˆ’ 1)) = (0...𝑁))
284283ineq1d 4211 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
285279, 284eqtr3id 2785 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ… = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
286285eqcomd 2737 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
287128fconst 6777 . . . . . . . . . . . . . . . . . 18 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0}
288 snssi 4811 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„š β†’ {0} βŠ† β„š)
28996, 97, 288mp2b 10 . . . . . . . . . . . . . . . . . . 19 {0} βŠ† β„š
290289, 93sstri 3991 . . . . . . . . . . . . . . . . . 18 {0} βŠ† β„‚
291 fss 6734 . . . . . . . . . . . . . . . . . 18 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„‚) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚)
292287, 290, 291mp2an 689 . . . . . . . . . . . . . . . . 17 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚
293 fun 6753 . . . . . . . . . . . . . . . . 17 (((𝑀:(0...𝑁)βŸΆβ„š ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
294292, 293mpanl2 698 . . . . . . . . . . . . . . . 16 ((𝑀:(0...𝑁)βŸΆβ„š ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
295286, 294sylan2 592 . . . . . . . . . . . . . . 15 ((𝑀:(0...𝑁)βŸΆβ„š ∧ πœ‘) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
296295ancoms 458 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
297 nn0uz 12869 . . . . . . . . . . . . . . . . . 18 β„•0 = (β„€β‰₯β€˜0)
2986, 297eleqtrdi 2842 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜0))
299 uzsplit 13578 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (β„€β‰₯β€˜0) β†’ (β„€β‰₯β€˜0) = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
300298, 299syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β„€β‰₯β€˜0) = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
301297, 300eqtrid 2783 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ β„•0 = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
302283uneq1d 4162 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
303301, 302eqtr2d 2772 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = β„•0)
304 ssequn1 4180 . . . . . . . . . . . . . . . . . 18 (β„š βŠ† β„‚ ↔ (β„š βˆͺ β„‚) = β„‚)
30593, 304mpbi 229 . . . . . . . . . . . . . . . . 17 (β„š βˆͺ β„‚) = β„‚
306305a1i 11 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β„š βˆͺ β„‚) = β„‚)
307303, 306feq23d 6712 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚) ↔ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚))
308307adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚) ↔ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚))
309296, 308mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚)
310 ffn 6717 . . . . . . . . . . . . . . . 16 (𝑀:(0...𝑁)βŸΆβ„š β†’ 𝑀 Fn (0...𝑁))
311 fnimadisj 6682 . . . . . . . . . . . . . . . 16 ((𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
312310, 286, 311syl2anr 596 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
3132nn0zd 12589 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 ∈ β„€)
314313peano2zd 12674 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ β„€)
315 uzid 12842 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ β„€ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)))
316 ne0i 4334 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)) β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
317314, 315, 3163syl 18 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
318 inidm 4218 . . . . . . . . . . . . . . . . . . 19 ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = (β„€β‰₯β€˜(𝑁 + 1))
319318neeq1i 3004 . . . . . . . . . . . . . . . . . 18 (((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ… ↔ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
320317, 319sylibr 233 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ…)
321 xpima2 6183 . . . . . . . . . . . . . . . . 17 (((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ… β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
322320, 321syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
323322adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
324312, 323uneq12d 4164 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1)))) = (βˆ… βˆͺ {0}))
325 imaundir 6150 . . . . . . . . . . . . . 14 ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))))
326 uncom 4153 . . . . . . . . . . . . . . 15 (βˆ… βˆͺ {0}) = ({0} βˆͺ βˆ…)
327 un0 4390 . . . . . . . . . . . . . . 15 ({0} βˆͺ βˆ…) = {0}
328326, 327eqtr2i 2760 . . . . . . . . . . . . . 14 {0} = (βˆ… βˆͺ {0})
329324, 325, 3283eqtr4g 2796 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
330286, 310anim12ci 613 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…))
331 fnconstg 6779 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1)))
332128, 331ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1))
333 fvun1 6982 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 Fn (0...𝑁) ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1)) ∧ (((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ… ∧ π‘˜ ∈ (0...𝑁))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
334332, 333mp3an2 1448 . . . . . . . . . . . . . . . . . . 19 ((𝑀 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ… ∧ π‘˜ ∈ (0...𝑁))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
335334anassrs 467 . . . . . . . . . . . . . . . . . 18 (((𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
336330, 335sylan 579 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
337336eqcomd 2737 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) = ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜))
338337oveq1d 7427 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = (((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
339338sumeq2dv 15654 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
340339mpteq2dv 5250 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜))))
341277, 276, 309, 329, 340coeeq 25977 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})))
342341reseq1d 5980 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)))
343 res0 5985 . . . . . . . . . . . . . 14 (𝑀 β†Ύ βˆ…) = βˆ…
344285reseq2d 5981 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑀 β†Ύ βˆ…) = (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
345 res0 5985 . . . . . . . . . . . . . . 15 (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ βˆ…) = βˆ…
346285reseq2d 5981 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ βˆ…) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
347345, 346eqtr3id 2785 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ… = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
348343, 344, 3473eqtr3a 2795 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
349 fss 6734 . . . . . . . . . . . . . . 15 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„š) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š)
350287, 289, 349mp2an 689 . . . . . . . . . . . . . 14 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š
351 fresaunres1 6764 . . . . . . . . . . . . . 14 ((𝑀:(0...𝑁)βŸΆβ„š ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š ∧ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
352350, 351mp3an2 1448 . . . . . . . . . . . . 13 ((𝑀:(0...𝑁)βŸΆβ„š ∧ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
353348, 352sylan2 592 . . . . . . . . . . . 12 ((𝑀:(0...𝑁)βŸΆβ„š ∧ πœ‘) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
354353ancoms 458 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
355342, 354eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀)
356 fveq2 6891 . . . . . . . . . . 11 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (coeffβ€˜0𝑝))
357356reseq1d 5980 . . . . . . . . . 10 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)))
358 eqtr2 2755 . . . . . . . . . . . 12 ((((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 ∧ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁))) β†’ 𝑀 = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)))
359 coe0 26006 . . . . . . . . . . . . . 14 (coeffβ€˜0𝑝) = (β„•0 Γ— {0})
360359reseq1i 5977 . . . . . . . . . . . . 13 ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) = ((β„•0 Γ— {0}) β†Ύ (0...𝑁))
361 elfznn0 13599 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (0...𝑁) β†’ π‘₯ ∈ β„•0)
362361ssriv 3986 . . . . . . . . . . . . . 14 (0...𝑁) βŠ† β„•0
363 xpssres 6018 . . . . . . . . . . . . . 14 ((0...𝑁) βŠ† β„•0 β†’ ((β„•0 Γ— {0}) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0}))
364362, 363ax-mp 5 . . . . . . . . . . . . 13 ((β„•0 Γ— {0}) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0})
365360, 364eqtri 2759 . . . . . . . . . . . 12 ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0})
366358, 365eqtrdi 2787 . . . . . . . . . . 11 ((((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 ∧ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁))) β†’ 𝑀 = ((0...𝑁) Γ— {0}))
367366ex 412 . . . . . . . . . 10 (((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 β†’ (((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) β†’ 𝑀 = ((0...𝑁) Γ— {0})))
368355, 357, 367syl2im 40 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ 𝑀 = ((0...𝑁) Γ— {0})))
369368necon3d 2960 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β‰  ((0...𝑁) Γ— {0}) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝))
370369impr 454 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝)
371 eldifsn 4790 . . . . . . 7 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}) ↔ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š) ∧ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝))
372278, 370, 371sylanbrc 582 . . . . . 6 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}))
373372adantrr 714 . . . . 5 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}))
374 oveq1 7419 . . . . . . . . . . . 12 (𝑦 = 𝐴 β†’ (π‘¦β†‘π‘˜) = (π΄β†‘π‘˜))
375374oveq2d 7428 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
376375sumeq2sdv 15655 . . . . . . . . . 10 (𝑦 = 𝐴 β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
377 eqid 2731 . . . . . . . . . 10 (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
378 sumex 15639 . . . . . . . . . 10 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) ∈ V
379376, 377, 378fvmpt 6998 . . . . . . . . 9 (𝐴 ∈ β„‚ β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
3801, 379syl 17 . . . . . . . 8 (πœ‘ β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
381380adantr 480 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
382107adantll 711 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
383 aacllem.2 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
384383adantlr 712 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
385110, 384mulcld 11239 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
386385adantllr 716 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
38751, 382, 386fsummulc2 15735 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
388 aacllem.4 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β†‘π‘˜) = Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋))
389388oveq2d 7428 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)))
390389adantlr 712 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)))
391382adantr 480 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
392110adantllr 716 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„‚)
393 simpll 764 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ πœ‘)
394393, 383sylan 579 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
395391, 392, 394mulassd 11242 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = ((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
396395sumeq2dv 15654 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
397387, 390, 3963eqtr4d 2781 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
398397sumeq2dv 15654 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
399107ad2ant2lr 745 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
400110anasss 466 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
401400adantlr 712 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
402399, 401mulcld 11239 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
403383ad2ant2rl 746 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝑋 ∈ β„‚)
404402, 403mulcld 11239 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) ∈ β„‚)
40543, 69, 404fsumcom 15726 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
406398, 405eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
407406adantrr 714 . . . . . . . . 9 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
408 nfv 1916 . . . . . . . . . . . 12 β„²π‘›πœ‘
409 nfv 1916 . . . . . . . . . . . . 13 Ⅎ𝑛 𝑀:(0...𝑁)βŸΆβ„š
410 nfra1 3280 . . . . . . . . . . . . 13 β„²π‘›βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0
411409, 410nfan 1901 . . . . . . . . . . . 12 Ⅎ𝑛(𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
412408, 411nfan 1901 . . . . . . . . . . 11 Ⅎ𝑛(πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
413 rspa 3244 . . . . . . . . . . . . . . . 16 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
414413oveq1d 7427 . . . . . . . . . . . . . . 15 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
415414adantll 711 . . . . . . . . . . . . . 14 (((𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
416415adantll 711 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
417383adantlr 712 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
41892, 417, 113fsummulc1 15736 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
419418adantlrr 718 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
420383mul02d 11417 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (0 Β· 𝑋) = 0)
421420adantlr 712 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (0 Β· 𝑋) = 0)
422416, 419, 4213eqtr3d 2779 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0)
423422ex 412 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ (𝑛 ∈ (1...𝑁) β†’ Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0))
424412, 423ralrimi 3253 . . . . . . . . . 10 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0)
425424sumeq2d 15653 . . . . . . . . 9 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426407, 425eqtrd 2771 . . . . . . . 8 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)0)
42722olci 863 . . . . . . . . 9 ((1...𝑁) βŠ† (β„€β‰₯β€˜π΅) ∨ (1...𝑁) ∈ Fin)
428 sumz 15673 . . . . . . . . 9 (((1...𝑁) βŠ† (β„€β‰₯β€˜π΅) ∨ (1...𝑁) ∈ Fin) β†’ Σ𝑛 ∈ (1...𝑁)0 = 0)
429427, 428ax-mp 5 . . . . . . . 8 Σ𝑛 ∈ (1...𝑁)0 = 0
430426, 429eqtrdi 2787 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = 0)
431381, 430eqtrd 2771 . . . . . 6 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0)
432431adantrlr 720 . . . . 5 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0)
433 fveq1 6890 . . . . . . 7 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ (π‘₯β€˜π΄) = ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄))
434433eqeq1d 2733 . . . . . 6 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ ((π‘₯β€˜π΄) = 0 ↔ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0))
435434rspcev 3612 . . . . 5 (((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}) ∧ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
436373, 432, 435syl2anc 583 . . . 4 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
437274, 436sylanr1 679 . . 3 ((πœ‘ ∧ (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
438271, 437rexlimddv 3160 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
439 elqaa 26072 . 2 (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ β„‚ ∧ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0))
4401, 438, 439sylanbrc 582 1 (πœ‘ β†’ 𝐴 ∈ 𝔸)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   β‰  wne 2939   βˆ‰ wnel 3045  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7412   ∘f cof 7671   ↑m cmap 8823   β‰ˆ cen 8939   β‰Ό cdom 8940  Fincfn 8942  β„‚cc 11111  0cc0 11113  1c1 11114   + caddc 11116   Β· cmul 11118   < clt 11253   ≀ cle 11254   βˆ’ cmin 11449  β„•0cn0 12477  β„€cz 12563  β„€β‰₯cuz 12827  β„šcq 12937  ...cfz 13489  β†‘cexp 14032  β™―chash 14295  Ξ£csu 15637  Basecbs 17149   β†Ύs cress 17178  .rcmulr 17203  Scalarcsca 17205   ·𝑠 cvsca 17206  0gc0g 17390   Ξ£g cgsu 17391  Moorecmre 17531  mrClscmrc 17532  mrIndcmri 17533  ACScacs 17534  Ringcrg 20128  NzRingcnzr 20404  DivRingcdr 20501  LModclmod 20615  LSubSpclss 20687  LSpanclspn 20727  LBasisclbs 20830  LVecclvec 20858  β„‚fldccnfld 21145   freeLMod cfrlm 21521   unitVec cuvc 21557   LIndF clindf 21579  LIndSclinds 21580  0𝑝c0p 25419  Polycply 25934  coeffccoe 25936  π”Έcaa 26064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7728  ax-inf2 9639  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191  ax-addf 11192  ax-mulf 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7673  df-om 7859  df-1st 7978  df-2nd 7979  df-supp 8150  df-tpos 8214  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-oadd 8473  df-er 8706  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9365  df-sup 9440  df-inf 9441  df-oi 9508  df-card 9937  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-xnn0 12550  df-z 12564  df-dec 12683  df-uz 12828  df-q 12938  df-rp 12980  df-fz 13490  df-fzo 13633  df-fl 13762  df-mod 13840  df-seq 13972  df-exp 14033  df-hash 14296  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-clim 15437  df-rlim 15438  df-sum 15638  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-0g 17392  df-gsum 17393  df-prds 17398  df-pws 17400  df-mre 17535  df-mrc 17536  df-mri 17537  df-acs 17538  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-mhm 18706  df-submnd 18707  df-grp 18859  df-minusg 18860  df-sbg 18861  df-mulg 18988  df-subg 19040  df-ghm 19129  df-cntz 19223  df-cmn 19692  df-abl 19693  df-mgp 20030  df-rng 20048  df-ur 20077  df-ring 20130  df-cring 20131  df-oppr 20226  df-dvdsr 20249  df-unit 20250  df-invr 20280  df-dvr 20293  df-nzr 20405  df-subrng 20435  df-subrg 20460  df-drng 20503  df-lmod 20617  df-lss 20688  df-lsp 20728  df-lmhm 20778  df-lbs 20831  df-lvec 20859  df-sra 20931  df-rgmod 20932  df-cnfld 21146  df-dsmm 21507  df-frlm 21522  df-uvc 21558  df-lindf 21581  df-linds 21582  df-0p 25420  df-ply 25938  df-coe 25940  df-dgr 25941  df-aa 26065
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator