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 47801
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 12529 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ)
43ltp1d 12140 . . . . 5 (πœ‘ β†’ 𝑁 < (𝑁 + 1))
5 peano2nn0 12508 . . . . . . . 8 (𝑁 ∈ β„•0 β†’ (𝑁 + 1) ∈ β„•0)
62, 5syl 17 . . . . . . 7 (πœ‘ β†’ (𝑁 + 1) ∈ β„•0)
76nn0red 12529 . . . . . 6 (πœ‘ β†’ (𝑁 + 1) ∈ ℝ)
83, 7ltnled 11357 . . . . 5 (πœ‘ β†’ (𝑁 < (𝑁 + 1) ↔ Β¬ (𝑁 + 1) ≀ 𝑁))
94, 8mpbid 231 . . . 4 (πœ‘ β†’ Β¬ (𝑁 + 1) ≀ 𝑁)
10 aacllem.3 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
11103expa 1118 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
1211fmpttd 7111 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
13 qex 12941 . . . . . . . . . . 11 β„š ∈ V
14 ovex 7438 . . . . . . . . . . 11 (1...𝑁) ∈ V
1513, 14elmap 8861 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐢):(1...𝑁)βŸΆβ„š)
1612, 15sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
1716fmpttd 7111 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)⟢(β„š ↑m (1...𝑁)))
18 eqid 2732 . . . . . . . . . . . 12 (β„‚fld β†Ύs β„š) = (β„‚fld β†Ύs β„š)
1918qdrng 27112 . . . . . . . . . . 11 (β„‚fld β†Ύs β„š) ∈ DivRing
20 drngring 20314 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ Ring)
2119, 20ax-mp 5 . . . . . . . . . 10 (β„‚fld β†Ύs β„š) ∈ Ring
22 fzfi 13933 . . . . . . . . . 10 (1...𝑁) ∈ Fin
23 eqid 2732 . . . . . . . . . . 11 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) = ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))
2423frlmlmod 21295 . . . . . . . . . 10 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod)
2521, 22, 24mp2an 690 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod
26 fzfi 13933 . . . . . . . . 9 (0...𝑁) ∈ Fin
2718qrngbas 27111 . . . . . . . . . . . 12 β„š = (Baseβ€˜(β„‚fld β†Ύs β„š))
2823, 27frlmfibas 21308 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (1...𝑁) ∈ Fin) β†’ (β„š ↑m (1...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
2919, 22, 28mp2an 690 . . . . . . . . . 10 (β„š ↑m (1...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
3023frlmsca 21299 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (1...𝑁) ∈ Fin) β†’ (β„‚fld β†Ύs β„š) = (Scalarβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
3119, 22, 30mp2an 690 . . . . . . . . . 10 (β„‚fld β†Ύs β„š) = (Scalarβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
32 eqid 2732 . . . . . . . . . 10 ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
3318qrng0 27113 . . . . . . . . . . . 12 0 = (0gβ€˜(β„‚fld β†Ύs β„š))
3423, 33frlm0 21300 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((1...𝑁) Γ— {0}) = (0gβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
3521, 22, 34mp2an 690 . . . . . . . . . 10 ((1...𝑁) Γ— {0}) = (0gβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
36 eqid 2732 . . . . . . . . . . . 12 ((β„‚fld β†Ύs β„š) freeLMod (0...𝑁)) = ((β„‚fld β†Ύs β„š) freeLMod (0...𝑁))
3736, 27frlmfibas 21308 . . . . . . . . . . 11 (((β„‚fld β†Ύs β„š) ∈ DivRing ∧ (0...𝑁) ∈ Fin) β†’ (β„š ↑m (0...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (0...𝑁))))
3819, 26, 37mp2an 690 . . . . . . . . . 10 (β„š ↑m (0...𝑁)) = (Baseβ€˜((β„‚fld β†Ύs β„š) freeLMod (0...𝑁)))
3929, 31, 32, 35, 33, 38islindf4 21384 . . . . . . . . 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 1451 . . . . . . . 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 8839 . . . . . . . . 9 (𝑀 ∈ (β„š ↑m (0...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
43 fzfid 13934 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (0...𝑁) ∈ Fin)
44 fvexd 6903 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
4514mptex 7221 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V
4645a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ V)
47 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
4847feqmptd 6957 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑀 = (π‘˜ ∈ (0...𝑁) ↦ (π‘€β€˜π‘˜)))
49 eqidd 2733 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
5043, 44, 46, 48, 49offval2 7686 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢))))
51 fzfid 13934 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (1...𝑁) ∈ Fin)
52 ffvelcdm 7080 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5352adantll 712 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
5416adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) ∈ (β„š ↑m (1...𝑁)))
55 cnfldmul 20942 . . . . . . . . . . . . . . . . . . . . . 22 Β· = (.rβ€˜β„‚fld)
5618, 55ressmulr 17248 . . . . . . . . . . . . . . . . . . . . 21 (β„š ∈ V β†’ Β· = (.rβ€˜(β„‚fld β†Ύs β„š)))
5713, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Β· = (.rβ€˜(β„‚fld β†Ύs β„š))
5823, 29, 27, 51, 53, 54, 32, 57frlmvscafval 21312 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
59 fvexd 6903 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ V)
6011adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„š)
61 fconstmpt 5736 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜))
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) = (𝑛 ∈ (1...𝑁) ↦ (π‘€β€˜π‘˜)))
63 eqidd 2733 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ 𝐢) = (𝑛 ∈ (1...𝑁) ↦ 𝐢))
6451, 59, 60, 62, 63offval2 7686 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (((1...𝑁) Γ— {(π‘€β€˜π‘˜)}) ∘f Β· (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6558, 64eqtrd 2772 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
6665mpteq2dva 5247 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜)( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
6750, 66eqtrd 2772 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
6867oveq2d 7421 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
69 fzfid 13934 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (1...𝑁) ∈ Fin)
7021a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (β„‚fld β†Ύs β„š) ∈ Ring)
7153adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„š)
7211an32s 650 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„š)
7372adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„š)
74 qmulcl 12947 . . . . . . . . . . . . . . . . . . . 20 (((π‘€β€˜π‘˜) ∈ β„š ∧ 𝐢 ∈ β„š) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7571, 73, 74syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7675an32s 650 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
7776fmpttd 7111 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7813, 14elmap 8861 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
7977, 78sylibr 233 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)))
80 eqid 2732 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))
8114mptex 7221 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)) ∈ V)
83 snex 5430 . . . . . . . . . . . . . . . . . . 19 {0} ∈ V
8414, 83xpex 7736 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) Γ— {0}) ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((1...𝑁) Γ— {0}) ∈ V)
8680, 43, 82, 85fsuppmptdm 9370 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) finSupp ((1...𝑁) Γ— {0}))
8723, 29, 35, 69, 43, 70, 79, 86frlmgsum 21318 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))))
88 cnfldbas 20940 . . . . . . . . . . . . . . . . . 18 β„‚ = (Baseβ€˜β„‚fld)
89 cnfldadd 20941 . . . . . . . . . . . . . . . . . 18 + = (+gβ€˜β„‚fld)
90 cnfldex 20939 . . . . . . . . . . . . . . . . . . 19 β„‚fld ∈ V
9190a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„‚fld ∈ V)
92 fzfid 13934 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (0...𝑁) ∈ Fin)
93 qsscn 12940 . . . . . . . . . . . . . . . . . . 19 β„š βŠ† β„‚
9493a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ β„š βŠ† β„‚)
9575fmpttd 7111 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)):(0...𝑁)βŸΆβ„š)
96 0z 12565 . . . . . . . . . . . . . . . . . . . 20 0 ∈ β„€
97 zq 12934 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„€ β†’ 0 ∈ β„š)
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . 19 0 ∈ β„š
9998a1i 11 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 0 ∈ β„š)
100 addlid 11393 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (0 + π‘₯) = π‘₯)
101 addrid 11390 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ β„‚ β†’ (π‘₯ + 0) = π‘₯)
102100, 101jca 512 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ β„‚ β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
103102adantl 482 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ β„‚) β†’ ((0 + π‘₯) = π‘₯ ∧ (π‘₯ + 0) = π‘₯))
10488, 89, 18, 91, 92, 94, 95, 99, 103gsumress 18597 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))))
105 simplr 767 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑀:(0...𝑁)βŸΆβ„š)
106 qcn 12943 . . . . . . . . . . . . . . . . . . . . 21 ((π‘€β€˜π‘˜) ∈ β„š β†’ (π‘€β€˜π‘˜) ∈ β„‚)
10752, 106syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑀:(0...𝑁)βŸΆβ„š ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
108105, 107sylan 580 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
109 qcn 12943 . . . . . . . . . . . . . . . . . . . . . 22 (𝐢 ∈ β„š β†’ 𝐢 ∈ β„‚)
11011, 109syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„‚)
111110an32s 650 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
112111adantllr 717 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝐢 ∈ β„‚)
113108, 112mulcld 11230 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
11492, 113gsumfsum 21004 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
115104, 114eqtr3d 2774 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢))) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
116115mpteq2dva 5247 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ ((β„‚fld β†Ύs β„š) Ξ£g (π‘˜ ∈ (0...𝑁) ↦ ((π‘€β€˜π‘˜) Β· 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)))
11768, 87, 1163eqtrd 2776 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)))
118 qaddcl 12945 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š) β†’ (π‘₯ + 𝑦) ∈ β„š)
119118adantl 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) ∧ (π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š)) β†’ (π‘₯ + 𝑦) ∈ β„š)
12094, 119, 92, 75, 99fsumcllem 15674 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„š)
121120fmpttd 7111 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
12213, 14elmap 8861 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)):(1...𝑁)βŸΆβ„š)
123121, 122sylibr 233 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) ∈ (β„š ↑m (1...𝑁)))
124117, 123eqeltrd 2833 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))) ∈ (β„š ↑m (1...𝑁)))
125 elmapi 8839 . . . . . . . . . . . . 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 6714 . . . . . . . . . . . . 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 11204 . . . . . . . . . . . . 13 0 ∈ V
129 fnconstg 6776 . . . . . . . . . . . . 13 (0 ∈ V β†’ ((1...𝑁) Γ— {0}) Fn (1...𝑁))
130128, 129ax-mp 5 . . . . . . . . . . . 12 ((1...𝑁) Γ— {0}) Fn (1...𝑁)
131 nfcv 2903 . . . . . . . . . . . . . 14 Ⅎ𝑛((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))
132 nfcv 2903 . . . . . . . . . . . . . 14 Ⅎ𝑛 Ξ£g
133 nfcv 2903 . . . . . . . . . . . . . . 15 Ⅎ𝑛𝑀
134 nfcv 2903 . . . . . . . . . . . . . . 15 Ⅎ𝑛 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
135 nfcv 2903 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(0...𝑁)
136 nfmpt1 5255 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐢)
137135, 136nfmpt 5254 . . . . . . . . . . . . . . 15 Ⅎ𝑛(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
138133, 134, 137nfov 7435 . . . . . . . . . . . . . 14 Ⅎ𝑛(𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
139131, 132, 138nfov 7435 . . . . . . . . . . . . 13 Ⅎ𝑛(((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))
140 nfcv 2903 . . . . . . . . . . . . 13 Ⅎ𝑛((1...𝑁) Γ— {0})
141139, 140eqfnfv2f 7033 . . . . . . . . . . . 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 586 . . . . . . . . . . 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 6890 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›))
144 sumex 15630 . . . . . . . . . . . . . . 15 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ V
145 eqid 2732 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢)) = (𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
146145fvmpt2 7006 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) ∈ V) β†’ ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
147144, 146mpan2 689 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 ∈ (1...𝑁) ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
148143, 147sylan9eq 2792 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢))
149128fvconst2 7201 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {0})β€˜π‘›) = 0)
150149adantl 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((1...𝑁) Γ— {0})β€˜π‘›) = 0)
151148, 150eqeq12d 2748 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = (((1...𝑁) Γ— {0})β€˜π‘›) ↔ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
152151ralbidva 3175 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (βˆ€π‘› ∈ (1...𝑁)((((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) Ξ£g (𝑀 ∘f ( ·𝑠 β€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))(π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))))β€˜π‘›) = (((1...𝑁) Γ— {0})β€˜π‘›) ↔ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
153142, 152bitrd 278 . . . . . . . . . 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 593 . . . . . . . 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 3175 . . . . . . 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 278 . . . . . 6 (πœ‘ β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0}))))
158 drngnzr 20327 . . . . . . . . 9 ((β„‚fld β†Ύs β„š) ∈ DivRing β†’ (β„‚fld β†Ύs β„š) ∈ NzRing)
15919, 158ax-mp 5 . . . . . . . 8 (β„‚fld β†Ύs β„š) ∈ NzRing
16031islindf3 21372 . . . . . . . 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 690 . . . . . . 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 2732 . . . . . . . . . 10 (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
16345, 162dmmpti 6691 . . . . . . . . 9 dom (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) = (0...𝑁)
164 f1eq2 6780 . . . . . . . . 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 624 . . . . . . 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 274 . . . . . 6 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) LIndF ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ↔ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
168 con34b 315 . . . . . . . . 9 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ (Β¬ 𝑀 = ((0...𝑁) Γ— {0}) β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
169 df-nel 3047 . . . . . . . . . . 11 (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} ↔ Β¬ 𝑀 ∈ {((0...𝑁) Γ— {0})})
170 velsn 4643 . . . . . . . . . . 11 (𝑀 ∈ {((0...𝑁) Γ— {0})} ↔ 𝑀 = ((0...𝑁) Γ— {0}))
171169, 170xchbinx 333 . . . . . . . . . 10 (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} ↔ Β¬ 𝑀 = ((0...𝑁) Γ— {0}))
172171imbi1i 349 . . . . . . . . 9 ((𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ↔ (Β¬ 𝑀 = ((0...𝑁) Γ— {0}) β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
173168, 172bitr4i 277 . . . . . . . 8 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ (𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
174173ralbii 3093 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
175 raldifb 4143 . . . . . . 7 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(𝑀 βˆ‰ {((0...𝑁) Γ— {0})} β†’ Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ↔ βˆ€π‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
176 ralnex 3072 . . . . . . 7 (βˆ€π‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) Β¬ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ↔ Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
177174, 175, 1763bitri 296 . . . . . 6 (βˆ€π‘€ ∈ (β„š ↑m (0...𝑁))(βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ 𝑀 = ((0...𝑁) Γ— {0})) ↔ Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
178157, 167, 1773bitr3g 312 . . . . 5 (πœ‘ β†’ (((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) ↔ Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
179 eqid 2732 . . . . . . . . . . . . 13 (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
18029, 179lssmre 20569 . . . . . . . . . . . 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 2732 . . . . . . . . . . . 12 (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
184 eqid 2732 . . . . . . . . . . . 12 (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) = (mrClsβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
185179, 183, 184mrclsp 20592 . . . . . . . . . . 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 2732 . . . . . . . . . 10 (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) = (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
18831islvec 20707 . . . . . . . . . . . . 13 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec ↔ (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ DivRing))
18925, 19, 188mpbir2an 709 . . . . . . . . . . . 12 ((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LVec
190179, 186, 29lssacsex 20749 . . . . . . . . . . . . 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 496 . . . . . . . . . . . 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 6722 . . . . . . . . . . . 12 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† (β„š ↑m (1...𝑁)))
195 dif0 4371 . . . . . . . . . . . 12 ((β„š ↑m (1...𝑁)) βˆ– βˆ…) = (β„š ↑m (1...𝑁))
196194, 195sseqtrrdi 4032 . . . . . . . . . . 11 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…))
197196adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((β„š ↑m (1...𝑁)) βˆ– βˆ…))
198 eqid 2732 . . . . . . . . . . . . . . 15 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) = ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
199198, 23, 29uvcff 21337 . . . . . . . . . . . . . 14 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)):(1...𝑁)⟢(β„š ↑m (1...𝑁)))
20021, 22, 199mp2an 690 . . . . . . . . . . . . 13 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)):(1...𝑁)⟢(β„š ↑m (1...𝑁))
201 frn 6721 . . . . . . . . . . . . 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 4018 . . . . . . . . . . 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 4389 . . . . . . . . . . . . . 14 (ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…) = ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
206205fveq2i 6891 . . . . . . . . . . . . 13 ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)) = ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
207 eqid 2732 . . . . . . . . . . . . . . . 16 (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) = (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
20823, 198, 207frlmlbs 21343 . . . . . . . . . . . . . . 15 (((β„‚fld β†Ύs β„š) ∈ Ring ∧ (1...𝑁) ∈ Fin) β†’ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))
20921, 22, 208mp2an 690 . . . . . . . . . . . . . 14 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ (LBasisβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))
21029, 207, 183lbssp 20682 . . . . . . . . . . . . . 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 2760 . . . . . . . . . . . 12 ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)) = (β„š ↑m (1...𝑁))
213194, 212sseqtrrdi 4032 . . . . . . . . . . 11 (πœ‘ β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)))
214213adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βŠ† ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) βˆͺ βˆ…)))
215 un0 4389 . . . . . . . . . . 11 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆͺ βˆ…) = ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))
21625, 159pm3.2i 471 . . . . . . . . . . . . . 14 (((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)) ∈ LMod ∧ (β„‚fld β†Ύs β„š) ∈ NzRing)
217183, 31lindsind2 21365 . . . . . . . . . . . . . 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 1448 . . . . . . . . . . . . 13 ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∧ π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢))) β†’ Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
219218ralrimiva 3146 . . . . . . . . . . . 12 (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) β†’ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯})))
220186, 187ismri2 17572 . . . . . . . . . . . . . 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 587 . . . . . . . . . . . . 13 (πœ‘ β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) ↔ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯}))))
222221biimpar 478 . . . . . . . . . . . 12 ((πœ‘ ∧ βˆ€π‘₯ ∈ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) Β¬ π‘₯ ∈ ((LSpanβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))β€˜(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆ– {π‘₯}))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
223219, 222sylan2 593 . . . . . . . . . . 11 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
224215, 223eqeltrid 2837 . . . . . . . . . 10 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))))
225 mptfi 9347 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin)
226 rnfi 9331 . . . . . . . . . . . . 13 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin)
22726, 225, 226mp2b 10 . . . . . . . . . . . 12 ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ Fin
228227orci 863 . . . . . . . . . . 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 17588 . . . . . . . . 9 ((πœ‘ ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ βˆƒπ‘£ ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))(ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))))
231230ex 413 . . . . . . . 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 7438 . . . . . . . . . . . . 13 ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
233232rnex 7899 . . . . . . . . . . . 12 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∈ V
234 elpwi 4608 . . . . . . . . . . . 12 (𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β†’ 𝑣 βŠ† ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
235 ssdomg 8992 . . . . . . . . . . . 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 9004 . . . . . . . . . . . . . 14 ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
238237ancoms 459 . . . . . . . . . . . . 13 ((𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣) β†’ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
239 f1f1orn 6841 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1-ontoβ†’ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)))
240 ovex 7438 . . . . . . . . . . . . . . . . 17 (0...𝑁) ∈ V
241240f1oen 8965 . . . . . . . . . . . . . . . 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 9004 . . . . . . . . . . . . . . . . 17 (((0...𝑁) β‰ˆ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
244198uvcendim 21393 . . . . . . . . . . . . . . . . . . . 20 (((β„‚fld β†Ύs β„š) ∈ NzRing ∧ (1...𝑁) ∈ Fin) β†’ (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)))
245159, 22, 244mp2an 690 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) β‰ˆ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))
246245ensymi 8996 . . . . . . . . . . . . . . . . . 18 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)
247 domentr 9005 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)) β†’ (0...𝑁) β‰Ό (1...𝑁))
248 hashdom 14335 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) β†’ ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁)))
24926, 22, 248mp2an 690 . . . . . . . . . . . . . . . . . . . 20 ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (0...𝑁) β‰Ό (1...𝑁))
250 hashfz0 14388 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
2512, 250syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(0...𝑁)) = (𝑁 + 1))
252 hashfz1 14302 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ β„•0 β†’ (β™―β€˜(1...𝑁)) = 𝑁)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β™―β€˜(1...𝑁)) = 𝑁)
254251, 253breq12d 5160 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((β™―β€˜(0...𝑁)) ≀ (β™―β€˜(1...𝑁)) ↔ (𝑁 + 1) ≀ 𝑁))
255249, 254bitr3id 284 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((0...𝑁) β‰Ό (1...𝑁) ↔ (𝑁 + 1) ≀ 𝑁))
256247, 255imbitrid 243 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((0...𝑁) β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) ∧ ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁)) β‰ˆ (1...𝑁)) β†’ (𝑁 + 1) ≀ 𝑁))
257246, 256mpan2i 695 . . . . . . . . . . . . . . . . 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 416 . . . . . . . . . . . . . . 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 453 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑣 β‰Ό ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
264236, 263sylan2 593 . . . . . . . . . 10 ((πœ‘ ∧ 𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ (ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
265264adantrd 492 . . . . . . . . 9 ((πœ‘ ∧ 𝑣 ∈ 𝒫 ran ((β„‚fld β†Ύs β„š) unitVec (1...𝑁))) β†’ ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) β‰ˆ 𝑣 ∧ (𝑣 βˆͺ βˆ…) ∈ (mrIndβ€˜(LSubSpβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))))) β†’ ((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V β†’ (𝑁 + 1) ≀ 𝑁)))
266265rexlimdva 3155 . . . . . . . 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 411 . . . . . 6 (πœ‘ β†’ ((ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁))) ∧ (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V) β†’ (𝑁 + 1) ≀ 𝑁))
269268ancomsd 466 . . . . 5 (πœ‘ β†’ (((π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)):(0...𝑁)–1-1β†’V ∧ ran (π‘˜ ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐢)) ∈ (LIndSβ€˜((β„‚fld β†Ύs β„š) freeLMod (1...𝑁)))) β†’ (𝑁 + 1) ≀ 𝑁))
270178, 269sylbird 259 . . . 4 (πœ‘ β†’ (Β¬ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 β†’ (𝑁 + 1) ≀ 𝑁))
2719, 270mt3d 148 . . 3 (πœ‘ β†’ βˆƒπ‘€ ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})})βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
272 eldifsn 4789 . . . . 5 (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) ↔ (𝑀 ∈ (β„š ↑m (0...𝑁)) ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
27342anim1i 615 . . . . 5 ((𝑀 ∈ (β„š ↑m (0...𝑁)) ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) β†’ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
274272, 273sylbi 216 . . . 4 (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) β†’ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})))
27593a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ β„š βŠ† β„‚)
2762adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ 𝑁 ∈ β„•0)
277275, 276, 53elplyd 25707 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
278277adantrr 715 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š))
279 uzdisj 13570 . . . . . . . . . . . . . . . . . 18 ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…
2802nn0cnd 12530 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ β„‚)
281 pncan1 11634 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„‚ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
283282oveq2d 7421 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (0...((𝑁 + 1) βˆ’ 1)) = (0...𝑁))
284283ineq1d 4210 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
285279, 284eqtr3id 2786 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ… = ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))
286285eqcomd 2738 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
287128fconst 6774 . . . . . . . . . . . . . . . . . 18 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0}
288 snssi 4810 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„š β†’ {0} βŠ† β„š)
28996, 97, 288mp2b 10 . . . . . . . . . . . . . . . . . . 19 {0} βŠ† β„š
290289, 93sstri 3990 . . . . . . . . . . . . . . . . . 18 {0} βŠ† β„‚
291 fss 6731 . . . . . . . . . . . . . . . . . 18 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„‚) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚)
292287, 290, 291mp2an 690 . . . . . . . . . . . . . . . . 17 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚
293 fun 6750 . . . . . . . . . . . . . . . . 17 (((𝑀:(0...𝑁)βŸΆβ„š ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„‚) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
294292, 293mpanl2 699 . . . . . . . . . . . . . . . 16 ((𝑀:(0...𝑁)βŸΆβ„š ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
295286, 294sylan2 593 . . . . . . . . . . . . . . 15 ((𝑀:(0...𝑁)βŸΆβ„š ∧ πœ‘) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
296295ancoms 459 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚))
297 nn0uz 12860 . . . . . . . . . . . . . . . . . 18 β„•0 = (β„€β‰₯β€˜0)
2986, 297eleqtrdi 2843 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜0))
299 uzsplit 13569 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (β„€β‰₯β€˜0) β†’ (β„€β‰₯β€˜0) = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
300298, 299syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β„€β‰₯β€˜0) = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
301297, 300eqtrid 2784 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ β„•0 = ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
302283uneq1d 4161 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((0...((𝑁 + 1) βˆ’ 1)) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))))
303301, 302eqtr2d 2773 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1))) = β„•0)
304 ssequn1 4179 . . . . . . . . . . . . . . . . . 18 (β„š βŠ† β„‚ ↔ (β„š βˆͺ β„‚) = β„‚)
30593, 304mpbi 229 . . . . . . . . . . . . . . . . 17 (β„š βˆͺ β„‚) = β„‚
306305a1i 11 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β„š βˆͺ β„‚) = β„‚)
307303, 306feq23d 6709 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚) ↔ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚))
308307adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):((0...𝑁) βˆͺ (β„€β‰₯β€˜(𝑁 + 1)))⟢(β„š βˆͺ β„‚) ↔ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚))
309296, 308mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})):β„•0βŸΆβ„‚)
310 ffn 6714 . . . . . . . . . . . . . . . 16 (𝑀:(0...𝑁)βŸΆβ„š β†’ 𝑀 Fn (0...𝑁))
311 fnimadisj 6679 . . . . . . . . . . . . . . . 16 ((𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
312310, 286, 311syl2anr 597 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…)
3132nn0zd 12580 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 ∈ β„€)
314313peano2zd 12665 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 + 1) ∈ β„€)
315 uzid 12833 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ β„€ β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)))
316 ne0i 4333 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (β„€β‰₯β€˜(𝑁 + 1)) β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
317314, 315, 3163syl 18 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
318 inidm 4217 . . . . . . . . . . . . . . . . . . 19 ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = (β„€β‰₯β€˜(𝑁 + 1))
319318neeq1i 3005 . . . . . . . . . . . . . . . . . 18 (((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ… ↔ (β„€β‰₯β€˜(𝑁 + 1)) β‰  βˆ…)
320317, 319sylibr 233 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ…)
321 xpima2 6180 . . . . . . . . . . . . . . . . 17 (((β„€β‰₯β€˜(𝑁 + 1)) ∩ (β„€β‰₯β€˜(𝑁 + 1))) β‰  βˆ… β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
322320, 321syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
323322adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
324312, 323uneq12d 4163 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1)))) = (βˆ… βˆͺ {0}))
325 imaundir 6147 . . . . . . . . . . . . . 14 ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = ((𝑀 β€œ (β„€β‰₯β€˜(𝑁 + 1))) βˆͺ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β€œ (β„€β‰₯β€˜(𝑁 + 1))))
326 uncom 4152 . . . . . . . . . . . . . . 15 (βˆ… βˆͺ {0}) = ({0} βˆͺ βˆ…)
327 un0 4389 . . . . . . . . . . . . . . 15 ({0} βˆͺ βˆ…) = {0}
328326, 327eqtr2i 2761 . . . . . . . . . . . . . 14 {0} = (βˆ… βˆͺ {0})
329324, 325, 3283eqtr4g 2797 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
330286, 310anim12ci 614 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…))
331 fnconstg 6776 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1)))
332128, 331ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1))
333 fvun1 6979 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 Fn (0...𝑁) ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) Fn (β„€β‰₯β€˜(𝑁 + 1)) ∧ (((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ… ∧ π‘˜ ∈ (0...𝑁))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
334332, 333mp3an2 1449 . . . . . . . . . . . . . . . . . . 19 ((𝑀 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ… ∧ π‘˜ ∈ (0...𝑁))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
335334anassrs 468 . . . . . . . . . . . . . . . . . 18 (((𝑀 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))) = βˆ…) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
336330, 335sylan 580 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) = (π‘€β€˜π‘˜))
337336eqcomd 2738 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) = ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜))
338337oveq1d 7420 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = (((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
339338sumeq2dv 15645 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
340339mpteq2dv 5249 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)(((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}))β€˜π‘˜) Β· (π‘¦β†‘π‘˜))))
341277, 276, 309, 329, 340coeeq 25732 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})))
342341reseq1d 5978 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)))
343 res0 5983 . . . . . . . . . . . . . 14 (𝑀 β†Ύ βˆ…) = βˆ…
344285reseq2d 5979 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑀 β†Ύ βˆ…) = (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
345 res0 5983 . . . . . . . . . . . . . . 15 (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ βˆ…) = βˆ…
346285reseq2d 5979 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ βˆ…) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
347345, 346eqtr3id 2786 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ… = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
348343, 344, 3473eqtr3a 2796 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))))
349 fss 6731 . . . . . . . . . . . . . . 15 ((((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))⟢{0} ∧ {0} βŠ† β„š) β†’ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š)
350287, 289, 349mp2an 690 . . . . . . . . . . . . . 14 ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š
351 fresaunres1 6761 . . . . . . . . . . . . . 14 ((𝑀:(0...𝑁)βŸΆβ„š ∧ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}):(β„€β‰₯β€˜(𝑁 + 1))βŸΆβ„š ∧ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
352350, 351mp3an2 1449 . . . . . . . . . . . . 13 ((𝑀:(0...𝑁)βŸΆβ„š ∧ (𝑀 β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1)))) = (((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0}) β†Ύ ((0...𝑁) ∩ (β„€β‰₯β€˜(𝑁 + 1))))) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
353348, 352sylan2 593 . . . . . . . . . . . 12 ((𝑀:(0...𝑁)βŸΆβ„š ∧ πœ‘) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
354353ancoms 459 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑀 βˆͺ ((β„€β‰₯β€˜(𝑁 + 1)) Γ— {0})) β†Ύ (0...𝑁)) = 𝑀)
355342, 354eqtrd 2772 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀)
356 fveq2 6888 . . . . . . . . . . 11 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ (coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) = (coeffβ€˜0𝑝))
357356reseq1d 5978 . . . . . . . . . 10 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)))
358 eqtr2 2756 . . . . . . . . . . . 12 ((((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 ∧ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁))) β†’ 𝑀 = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)))
359 coe0 25761 . . . . . . . . . . . . . 14 (coeffβ€˜0𝑝) = (β„•0 Γ— {0})
360359reseq1i 5975 . . . . . . . . . . . . 13 ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) = ((β„•0 Γ— {0}) β†Ύ (0...𝑁))
361 elfznn0 13590 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (0...𝑁) β†’ π‘₯ ∈ β„•0)
362361ssriv 3985 . . . . . . . . . . . . . 14 (0...𝑁) βŠ† β„•0
363 xpssres 6016 . . . . . . . . . . . . . 14 ((0...𝑁) βŠ† β„•0 β†’ ((β„•0 Γ— {0}) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0}))
364362, 363ax-mp 5 . . . . . . . . . . . . 13 ((β„•0 Γ— {0}) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0})
365360, 364eqtri 2760 . . . . . . . . . . . 12 ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) = ((0...𝑁) Γ— {0})
366358, 365eqtrdi 2788 . . . . . . . . . . 11 ((((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 ∧ ((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁))) β†’ 𝑀 = ((0...𝑁) Γ— {0}))
367366ex 413 . . . . . . . . . 10 (((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = 𝑀 β†’ (((coeffβ€˜(𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))) β†Ύ (0...𝑁)) = ((coeffβ€˜0𝑝) β†Ύ (0...𝑁)) β†’ 𝑀 = ((0...𝑁) Γ— {0})))
368355, 357, 367syl2im 40 . . . . . . . . 9 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = 0𝑝 β†’ 𝑀 = ((0...𝑁) Γ— {0})))
369368necon3d 2961 . . . . . . . 8 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ (𝑀 β‰  ((0...𝑁) Γ— {0}) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝))
370369impr 455 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝)
371 eldifsn 4789 . . . . . . 7 ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}) ↔ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ (Polyβ€˜β„š) ∧ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β‰  0𝑝))
372278, 370, 371sylanbrc 583 . . . . . 6 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0}))) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}))
373372adantrr 715 . . . . 5 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}))
374 oveq1 7412 . . . . . . . . . . . 12 (𝑦 = 𝐴 β†’ (π‘¦β†‘π‘˜) = (π΄β†‘π‘˜))
375374oveq2d 7421 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ ((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
376375sumeq2sdv 15646 . . . . . . . . . 10 (𝑦 = 𝐴 β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
377 eqid 2732 . . . . . . . . . 10 (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))
378 sumex 15630 . . . . . . . . . 10 Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) ∈ V
379376, 377, 378fvmpt 6995 . . . . . . . . 9 (𝐴 ∈ β„‚ β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
3801, 379syl 17 . . . . . . . 8 (πœ‘ β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
381380adantr 481 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)))
382107adantll 712 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
383 aacllem.2 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
384383adantlr 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
385110, 384mulcld 11230 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
386385adantllr 717 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝐢 Β· 𝑋) ∈ β„‚)
38751, 382, 386fsummulc2 15726 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
388 aacllem.4 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β†‘π‘˜) = Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋))
389388oveq2d 7421 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)))
390389adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = ((π‘€β€˜π‘˜) Β· Σ𝑛 ∈ (1...𝑁)(𝐢 Β· 𝑋)))
391382adantr 481 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
392110adantllr 717 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ β„‚)
393 simpll 765 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ πœ‘)
394393, 383sylan 580 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
395391, 392, 394mulassd 11233 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = ((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
396395sumeq2dv 15645 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)((π‘€β€˜π‘˜) Β· (𝐢 Β· 𝑋)))
397387, 390, 3963eqtr4d 2782 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
398397sumeq2dv 15645 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
399107ad2ant2lr 746 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
400110anasss 467 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
401400adantlr 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝐢 ∈ β„‚)
402399, 401mulcld 11230 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ ((π‘€β€˜π‘˜) Β· 𝐢) ∈ β„‚)
403383ad2ant2rl 747 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝑋 ∈ β„‚)
404402, 403mulcld 11230 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ (π‘˜ ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) β†’ (((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) ∈ β„‚)
40543, 69, 404fsumcom 15717 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
406398, 405eqtrd 2772 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
407406adantrr 715 . . . . . . . . 9 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
408 nfv 1917 . . . . . . . . . . . 12 β„²π‘›πœ‘
409 nfv 1917 . . . . . . . . . . . . 13 Ⅎ𝑛 𝑀:(0...𝑁)βŸΆβ„š
410 nfra1 3281 . . . . . . . . . . . . 13 β„²π‘›βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0
411409, 410nfan 1902 . . . . . . . . . . . 12 Ⅎ𝑛(𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
412408, 411nfan 1902 . . . . . . . . . . 11 Ⅎ𝑛(πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0))
413 rspa 3245 . . . . . . . . . . . . . . . 16 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)
414413oveq1d 7420 . . . . . . . . . . . . . . 15 ((βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0 ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
415414adantll 712 . . . . . . . . . . . . . 14 (((𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
416415adantll 712 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = (0 Β· 𝑋))
417383adantlr 713 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
41892, 417, 113fsummulc1 15727 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀:(0...𝑁)βŸΆβ„š) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
419418adantlrr 719 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋))
420383mul02d 11408 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (0 Β· 𝑋) = 0)
421420adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (0 Β· 𝑋) = 0)
422416, 419, 4213eqtr3d 2780 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) ∧ 𝑛 ∈ (1...𝑁)) β†’ Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0)
423422ex 413 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ (𝑛 ∈ (1...𝑁) β†’ Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0))
424412, 423ralrimi 3254 . . . . . . . . . 10 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = 0)
425424sumeq2d 15644 . . . . . . . . 9 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Σ𝑛 ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)(((π‘€β€˜π‘˜) Β· 𝐢) Β· 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426407, 425eqtrd 2772 . . . . . . . 8 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = Σ𝑛 ∈ (1...𝑁)0)
42722olci 864 . . . . . . . . 9 ((1...𝑁) βŠ† (β„€β‰₯β€˜π΅) ∨ (1...𝑁) ∈ Fin)
428 sumz 15664 . . . . . . . . 9 (((1...𝑁) βŠ† (β„€β‰₯β€˜π΅) ∨ (1...𝑁) ∈ Fin) β†’ Σ𝑛 ∈ (1...𝑁)0 = 0)
429427, 428ax-mp 5 . . . . . . . 8 Σ𝑛 ∈ (1...𝑁)0 = 0
430426, 429eqtrdi 2788 . . . . . . 7 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π΄β†‘π‘˜)) = 0)
431381, 430eqtrd 2772 . . . . . 6 ((πœ‘ ∧ (𝑀:(0...𝑁)βŸΆβ„š ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0)
432431adantrlr 721 . . . . 5 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0)
433 fveq1 6887 . . . . . . 7 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ (π‘₯β€˜π΄) = ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄))
434433eqeq1d 2734 . . . . . 6 (π‘₯ = (𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) β†’ ((π‘₯β€˜π΄) = 0 ↔ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0))
435434rspcev 3612 . . . . 5 (((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜))) ∈ ((Polyβ€˜β„š) βˆ– {0𝑝}) ∧ ((𝑦 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· (π‘¦β†‘π‘˜)))β€˜π΄) = 0) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
436373, 432, 435syl2anc 584 . . . 4 ((πœ‘ ∧ ((𝑀:(0...𝑁)βŸΆβ„š ∧ 𝑀 β‰  ((0...𝑁) Γ— {0})) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
437274, 436sylanr1 680 . . 3 ((πœ‘ ∧ (𝑀 ∈ ((β„š ↑m (0...𝑁)) βˆ– {((0...𝑁) Γ— {0})}) ∧ βˆ€π‘› ∈ (1...𝑁)Ξ£π‘˜ ∈ (0...𝑁)((π‘€β€˜π‘˜) Β· 𝐢) = 0)) β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
438271, 437rexlimddv 3161 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0)
439 elqaa 25826 . 2 (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ β„‚ ∧ βˆƒπ‘₯ ∈ ((Polyβ€˜β„š) βˆ– {0𝑝})(π‘₯β€˜π΄) = 0))
4401, 438, 439sylanbrc 583 1 (πœ‘ β†’ 𝐴 ∈ 𝔸)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940   βˆ‰ wnel 3046  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   Fn wfn 6535  βŸΆwf 6536  β€“1-1β†’wf1 6537  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7405   ∘f cof 7664   ↑m cmap 8816   β‰ˆ cen 8932   β‰Ό cdom 8933  Fincfn 8935  β„‚cc 11104  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  β„šcq 12928  ...cfz 13480  β†‘cexp 14023  β™―chash 14286  Ξ£csu 15628  Basecbs 17140   β†Ύs cress 17169  .rcmulr 17194  Scalarcsca 17196   ·𝑠 cvsca 17197  0gc0g 17381   Ξ£g cgsu 17382  Moorecmre 17522  mrClscmrc 17523  mrIndcmri 17524  ACScacs 17525  Ringcrg 20049  NzRingcnzr 20283  DivRingcdr 20307  LModclmod 20463  LSubSpclss 20534  LSpanclspn 20574  LBasisclbs 20677  LVecclvec 20705  β„‚fldccnfld 20936   freeLMod cfrlm 21292   unitVec cuvc 21328   LIndF clindf 21350  LIndSclinds 21351  0𝑝c0p 25177  Polycply 25689  coeffccoe 25691  π”Έcaa 25818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-tpos 8207  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-oadd 8466  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-rlim 15429  df-sum 15629  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mre 17526  df-mrc 17527  df-mri 17528  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-submnd 18668  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-ghm 19084  df-cntz 19175  df-cmn 19644  df-abl 19645  df-mgp 19982  df-ur 19999  df-ring 20051  df-cring 20052  df-oppr 20142  df-dvdsr 20163  df-unit 20164  df-invr 20194  df-dvr 20207  df-nzr 20284  df-drng 20309  df-subrg 20353  df-lmod 20465  df-lss 20535  df-lsp 20575  df-lmhm 20625  df-lbs 20678  df-lvec 20706  df-sra 20777  df-rgmod 20778  df-cnfld 20937  df-dsmm 21278  df-frlm 21293  df-uvc 21329  df-lindf 21352  df-linds 21353  df-0p 25178  df-ply 25693  df-coe 25695  df-dgr 25696  df-aa 25819
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator