Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ply1degltdimlem Structured version   Visualization version   GIF version

Theorem ply1degltdimlem 33252
Description: Lemma for ply1degltdim 33253. (Contributed by Thierry Arnoux, 20-Feb-2025.)
Hypotheses
Ref Expression
ply1degltdim.p 𝑃 = (Poly1𝑅)
ply1degltdim.d 𝐷 = ( deg1𝑅)
ply1degltdim.s 𝑆 = (𝐷 “ (-∞[,)𝑁))
ply1degltdim.n (𝜑𝑁 ∈ ℕ0)
ply1degltdim.r (𝜑𝑅 ∈ DivRing)
ply1degltdim.e 𝐸 = (𝑃s 𝑆)
ply1degltdimlem.f 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)))
Assertion
Ref Expression
ply1degltdimlem (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))
Distinct variable groups:   𝑛,𝐸   𝑛,𝐹   𝑛,𝑁   𝑃,𝑛   𝑅,𝑛   𝑆,𝑛   𝜑,𝑛
Allowed substitution hint:   𝐷(𝑛)

Proof of Theorem ply1degltdimlem
Dummy variables 𝑎 𝑖 𝑗 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ply1degltdim.p . . . . . 6 𝑃 = (Poly1𝑅)
2 eqid 2727 . . . . . 6 (Base‘𝑅) = (Base‘𝑅)
3 ply1degltdim.n . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
43ad3antrrr 729 . . . . . 6 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑁 ∈ ℕ0)
5 ply1degltdim.r . . . . . . . 8 (𝜑𝑅 ∈ DivRing)
65drngringd 20621 . . . . . . 7 (𝜑𝑅 ∈ Ring)
76ad3antrrr 729 . . . . . 6 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑅 ∈ Ring)
8 ply1degltdimlem.f . . . . . 6 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)))
9 eqid 2727 . . . . . 6 (0g𝑅) = (0g𝑅)
10 eqid 2727 . . . . . 6 (0g𝑃) = (0g𝑃)
11 elmapi 8859 . . . . . . . . 9 (𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
1211adantl 481 . . . . . . . 8 ((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
131ply1sca 22158 . . . . . . . . . . . 12 (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃))
145, 13syl 17 . . . . . . . . . . 11 (𝜑𝑅 = (Scalar‘𝑃))
1514fveq2d 6895 . . . . . . . . . 10 (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
1615adantr 480 . . . . . . . . 9 ((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
1716feq3d 6703 . . . . . . . 8 ((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → (𝑎:(0..^𝑁)⟶(Base‘𝑅) ↔ 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))))
1812, 17mpbird 257 . . . . . . 7 ((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
1918ad2antrr 725 . . . . . 6 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
20 simpr 484 . . . . . . 7 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸))
21 ovexd 7449 . . . . . . . 8 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → (0..^𝑁) ∈ V)
221, 5ply1lvec 33170 . . . . . . . . . . . 12 (𝜑𝑃 ∈ LVec)
2322lveclmodd 20981 . . . . . . . . . . 11 (𝜑𝑃 ∈ LMod)
24 ply1degltdim.d . . . . . . . . . . . 12 𝐷 = ( deg1𝑅)
25 ply1degltdim.s . . . . . . . . . . . 12 𝑆 = (𝐷 “ (-∞[,)𝑁))
261, 24, 25, 3, 6ply1degltlss 33199 . . . . . . . . . . 11 (𝜑𝑆 ∈ (LSubSp‘𝑃))
27 eqid 2727 . . . . . . . . . . . 12 (LSubSp‘𝑃) = (LSubSp‘𝑃)
2827lsssubg 20830 . . . . . . . . . . 11 ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃))
2923, 26, 28syl2anc 583 . . . . . . . . . 10 (𝜑𝑆 ∈ (SubGrp‘𝑃))
30 subgsubm 19094 . . . . . . . . . 10 (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃))
3129, 30syl 17 . . . . . . . . 9 (𝜑𝑆 ∈ (SubMnd‘𝑃))
3231ad3antrrr 729 . . . . . . . 8 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑆 ∈ (SubMnd‘𝑃))
33 eqid 2727 . . . . . . . . . . . . . . 15 (Base‘𝑃) = (Base‘𝑃)
3424, 1, 33deg1xrf 26004 . . . . . . . . . . . . . 14 𝐷:(Base‘𝑃)⟶ℝ*
35 ffn 6716 . . . . . . . . . . . . . 14 (𝐷:(Base‘𝑃)⟶ℝ*𝐷 Fn (Base‘𝑃))
3634, 35mp1i 13 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃))
37 eqid 2727 . . . . . . . . . . . . . 14 (Scalar‘𝑃) = (Scalar‘𝑃)
38 eqid 2727 . . . . . . . . . . . . . 14 ( ·𝑠𝑃) = ( ·𝑠𝑃)
39 eqid 2727 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
4023ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑃 ∈ LMod)
41 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘(Scalar‘𝑃)))
4233, 27lssss 20809 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃))
4326, 42syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑆 ⊆ (Base‘𝑃))
44 ply1degltdim.e . . . . . . . . . . . . . . . . . . 19 𝐸 = (𝑃s 𝑆)
4544, 33ressbas2 17209 . . . . . . . . . . . . . . . . . 18 (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸))
4643, 45syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 = (Base‘𝐸))
4746, 43eqsstrrd 4017 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃))
4847sselda 3978 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
4948adantlr 714 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
5033, 37, 38, 39, 40, 41, 49lmodvscld 20751 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·𝑠𝑃)𝑥) ∈ (Base‘𝑃))
51 mnfxr 11293 . . . . . . . . . . . . . . 15 -∞ ∈ ℝ*
5251a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈ ℝ*)
533nn0red 12555 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ)
5453rexrd 11286 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ*)
5554ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈ ℝ*)
5634a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ*)
5756, 50ffvelcdmd 7089 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠𝑃)𝑥)) ∈ ℝ*)
5857mnfled 13139 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·𝑠𝑃)𝑥)))
5956, 49ffvelcdmd 7089 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷𝑥) ∈ ℝ*)
606ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑅 ∈ Ring)
6115ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
6241, 61eleqtrrd 2831 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘𝑅))
631, 24, 60, 33, 2, 38, 62, 49deg1vscale 26027 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠𝑃)𝑥)) ≤ (𝐷𝑥))
64 simpll 766 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝜑)
65 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝐸))
6646ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑆 = (Base‘𝐸))
6765, 66eleqtrrd 2831 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥𝑆)
6851a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → -∞ ∈ ℝ*)
6954adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝑁 ∈ ℝ*)
7034, 35mp1i 13 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑆) → 𝐷 Fn (Base‘𝑃))
71 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝑆) → 𝑥𝑆)
7271, 25eleqtrdi 2838 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑆) → 𝑥 ∈ (𝐷 “ (-∞[,)𝑁)))
73 elpreima 7061 . . . . . . . . . . . . . . . . . . 19 (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷𝑥) ∈ (-∞[,)𝑁))))
7473simplbda 499 . . . . . . . . . . . . . . . . . 18 ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (𝐷 “ (-∞[,)𝑁))) → (𝐷𝑥) ∈ (-∞[,)𝑁))
7570, 72, 74syl2anc 583 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → (𝐷𝑥) ∈ (-∞[,)𝑁))
76 elico1 13391 . . . . . . . . . . . . . . . . . . 19 ((-∞ ∈ ℝ*𝑁 ∈ ℝ*) → ((𝐷𝑥) ∈ (-∞[,)𝑁) ↔ ((𝐷𝑥) ∈ ℝ* ∧ -∞ ≤ (𝐷𝑥) ∧ (𝐷𝑥) < 𝑁)))
7776biimpa 476 . . . . . . . . . . . . . . . . . 18 (((-∞ ∈ ℝ*𝑁 ∈ ℝ*) ∧ (𝐷𝑥) ∈ (-∞[,)𝑁)) → ((𝐷𝑥) ∈ ℝ* ∧ -∞ ≤ (𝐷𝑥) ∧ (𝐷𝑥) < 𝑁))
7877simp3d 1142 . . . . . . . . . . . . . . . . 17 (((-∞ ∈ ℝ*𝑁 ∈ ℝ*) ∧ (𝐷𝑥) ∈ (-∞[,)𝑁)) → (𝐷𝑥) < 𝑁)
7968, 69, 75, 78syl21anc 837 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑆) → (𝐷𝑥) < 𝑁)
8064, 67, 79syl2anc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷𝑥) < 𝑁)
8157, 59, 55, 63, 80xrlelttrd 13163 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠𝑃)𝑥)) < 𝑁)
8252, 55, 57, 58, 81elicod 13398 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠𝑃)𝑥)) ∈ (-∞[,)𝑁))
8336, 50, 82elpreimad 7062 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·𝑠𝑃)𝑥) ∈ (𝐷 “ (-∞[,)𝑁)))
8483, 25eleqtrrdi 2839 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·𝑠𝑃)𝑥) ∈ 𝑆)
8584anasss 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·𝑠𝑃)𝑥) ∈ 𝑆)
8685ad5ant15 758 . . . . . . . . 9 (((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·𝑠𝑃)𝑥) ∈ 𝑆)
8712ad2antrr 725 . . . . . . . . 9 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
8834, 35mp1i 13 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (0..^𝑁)) → 𝐷 Fn (Base‘𝑃))
89 eqid 2727 . . . . . . . . . . . . . . . 16 (mulGrp‘𝑃) = (mulGrp‘𝑃)
9089, 33mgpbas 20071 . . . . . . . . . . . . . . 15 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
91 eqid 2727 . . . . . . . . . . . . . . 15 (.g‘(mulGrp‘𝑃)) = (.g‘(mulGrp‘𝑃))
921ply1ring 22153 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
9389ringmgp 20170 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
946, 92, 933syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
9594adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd)
96 elfzonn0 13701 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ0)
9796adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ0)
98 eqid 2727 . . . . . . . . . . . . . . . . . 18 (var1𝑅) = (var1𝑅)
9998, 1, 33vr1cl 22123 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Ring → (var1𝑅) ∈ (Base‘𝑃))
1006, 99syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (var1𝑅) ∈ (Base‘𝑃))
101100adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → (var1𝑅) ∈ (Base‘𝑃))
10290, 91, 95, 97, 101mulgnn0cld 19041 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝑃))
10351a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → -∞ ∈ ℝ*)
10454adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ*)
10524, 1, 33deg1xrcl 26005 . . . . . . . . . . . . . . . 16 ((𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅))) ∈ ℝ*)
106102, 105syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅))) ∈ ℝ*)
107106mnfled 13139 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅))))
10896nn0red 12555 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ)
109108rexrd 11286 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ*)
110109adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ*)
11124, 1, 98, 89, 91deg1pwle 26042 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅))) ≤ 𝑛)
1126, 96, 111syl2an 595 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅))) ≤ 𝑛)
113 elfzolt2 13665 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁)
114113adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁)
115106, 110, 104, 112, 114xrlelttrd 13163 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅))) < 𝑁)
116103, 104, 106, 107, 115elicod 13398 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅))) ∈ (-∞[,)𝑁))
11788, 102, 116elpreimad 7062 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (𝐷 “ (-∞[,)𝑁)))
118117, 25eleqtrrdi 2839 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ 𝑆)
11946adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸))
120118, 119eleqtrd 2830 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝐸))
121120, 8fmptd 7118 . . . . . . . . . 10 (𝜑𝐹:(0..^𝑁)⟶(Base‘𝐸))
122121ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
123 inidm 4214 . . . . . . . . 9 ((0..^𝑁) ∩ (0..^𝑁)) = (0..^𝑁)
12486, 87, 122, 21, 21, 123off 7697 . . . . . . . 8 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → (𝑎f ( ·𝑠𝑃)𝐹):(0..^𝑁)⟶𝑆)
12521, 32, 124, 44gsumsubm 18778 . . . . . . 7 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)))
126 ringmnd 20174 . . . . . . . . . 10 (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
1276, 92, 1263syl 18 . . . . . . . . 9 (𝜑𝑃 ∈ Mnd)
12834, 35mp1i 13 . . . . . . . . . . 11 (𝜑𝐷 Fn (Base‘𝑃))
12933, 10mndidcl 18700 . . . . . . . . . . . 12 (𝑃 ∈ Mnd → (0g𝑃) ∈ (Base‘𝑃))
130127, 129syl 17 . . . . . . . . . . 11 (𝜑 → (0g𝑃) ∈ (Base‘𝑃))
13151a1i 11 . . . . . . . . . . . 12 (𝜑 → -∞ ∈ ℝ*)
13224, 1, 33deg1xrcl 26005 . . . . . . . . . . . . 13 ((0g𝑃) ∈ (Base‘𝑃) → (𝐷‘(0g𝑃)) ∈ ℝ*)
133130, 132syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐷‘(0g𝑃)) ∈ ℝ*)
134133mnfled 13139 . . . . . . . . . . . 12 (𝜑 → -∞ ≤ (𝐷‘(0g𝑃)))
13524, 1, 10deg1z 26010 . . . . . . . . . . . . . 14 (𝑅 ∈ Ring → (𝐷‘(0g𝑃)) = -∞)
1366, 135syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐷‘(0g𝑃)) = -∞)
13753mnfltd 13128 . . . . . . . . . . . . 13 (𝜑 → -∞ < 𝑁)
138136, 137eqbrtrd 5164 . . . . . . . . . . . 12 (𝜑 → (𝐷‘(0g𝑃)) < 𝑁)
139131, 54, 133, 134, 138elicod 13398 . . . . . . . . . . 11 (𝜑 → (𝐷‘(0g𝑃)) ∈ (-∞[,)𝑁))
140128, 130, 139elpreimad 7062 . . . . . . . . . 10 (𝜑 → (0g𝑃) ∈ (𝐷 “ (-∞[,)𝑁)))
141140, 25eleqtrrdi 2839 . . . . . . . . 9 (𝜑 → (0g𝑃) ∈ 𝑆)
14244, 33, 10ress0g 18713 . . . . . . . . 9 ((𝑃 ∈ Mnd ∧ (0g𝑃) ∈ 𝑆𝑆 ⊆ (Base‘𝑃)) → (0g𝑃) = (0g𝐸))
143127, 141, 43, 142syl3anc 1369 . . . . . . . 8 (𝜑 → (0g𝑃) = (0g𝐸))
144143ad3antrrr 729 . . . . . . 7 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → (0g𝑃) = (0g𝐸))
14520, 125, 1443eqtr4d 2777 . . . . . 6 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝑃))
1461, 2, 4, 7, 8, 9, 10, 19, 145ply1gsumz 33201 . . . . 5 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑎 = ((0..^𝑁) × {(0g𝑅)}))
14714fveq2d 6895 . . . . . . . 8 (𝜑 → (0g𝑅) = (0g‘(Scalar‘𝑃)))
148147sneqd 4636 . . . . . . 7 (𝜑 → {(0g𝑅)} = {(0g‘(Scalar‘𝑃))})
149148xpeq2d 5702 . . . . . 6 (𝜑 → ((0..^𝑁) × {(0g𝑅)}) = ((0..^𝑁) × {(0g‘(Scalar‘𝑃))}))
150149ad3antrrr 729 . . . . 5 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → ((0..^𝑁) × {(0g𝑅)}) = ((0..^𝑁) × {(0g‘(Scalar‘𝑃))}))
151146, 150eqtrd 2767 . . . 4 ((((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑎 = ((0..^𝑁) × {(0g‘(Scalar‘𝑃))}))
152151expl 457 . . 3 ((𝜑𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → ((𝑎 finSupp (0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑎 = ((0..^𝑁) × {(0g‘(Scalar‘𝑃))})))
153152ralrimiva 3141 . 2 (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))((𝑎 finSupp (0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑎 = ((0..^𝑁) × {(0g‘(Scalar‘𝑃))})))
154118, 8fmptd 7118 . . . . . 6 (𝜑𝐹:(0..^𝑁)⟶𝑆)
155154frnd 6724 . . . . 5 (𝜑 → ran 𝐹𝑆)
156 eqid 2727 . . . . . 6 (LSpan‘𝑃) = (LSpan‘𝑃)
15727, 156lspssp 20861 . . . . 5 ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
15823, 26, 155, 157syl3anc 1369 . . . 4 (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
159 breq1 5145 . . . . . . . 8 (𝑎 = ((coe1𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp (0g‘(Scalar‘𝑃)) ↔ ((coe1𝑥) ↾ (0..^𝑁)) finSupp (0g‘(Scalar‘𝑃))))
160 oveq1 7421 . . . . . . . . . 10 (𝑎 = ((coe1𝑥) ↾ (0..^𝑁)) → (𝑎f ( ·𝑠𝑃)𝐹) = (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹))
161160oveq2d 7430 . . . . . . . . 9 (𝑎 = ((coe1𝑥) ↾ (0..^𝑁)) → (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (𝑃 Σg (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹)))
162161eqeq2d 2738 . . . . . . . 8 (𝑎 = ((coe1𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σg (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹))))
163159, 162anbi12d 630 . . . . . . 7 (𝑎 = ((coe1𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp (0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹))) ↔ (((coe1𝑥) ↾ (0..^𝑁)) finSupp (0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹)))))
164 fvexd 6906 . . . . . . . 8 ((𝜑𝑥𝑆) → (Base‘(Scalar‘𝑃)) ∈ V)
165 ovexd 7449 . . . . . . . 8 ((𝜑𝑥𝑆) → (0..^𝑁) ∈ V)
16643sselda 3978 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → 𝑥 ∈ (Base‘𝑃))
167 eqid 2727 . . . . . . . . . . . 12 (coe1𝑥) = (coe1𝑥)
168167, 33, 1, 2coe1f 22117 . . . . . . . . . . 11 (𝑥 ∈ (Base‘𝑃) → (coe1𝑥):ℕ0⟶(Base‘𝑅))
169166, 168syl 17 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (coe1𝑥):ℕ0⟶(Base‘𝑅))
17015adantr 480 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
171170feq3d 6703 . . . . . . . . . 10 ((𝜑𝑥𝑆) → ((coe1𝑥):ℕ0⟶(Base‘𝑅) ↔ (coe1𝑥):ℕ0⟶(Base‘(Scalar‘𝑃))))
172169, 171mpbid 231 . . . . . . . . 9 ((𝜑𝑥𝑆) → (coe1𝑥):ℕ0⟶(Base‘(Scalar‘𝑃)))
173 fzo0ssnn0 13737 . . . . . . . . . 10 (0..^𝑁) ⊆ ℕ0
174173a1i 11 . . . . . . . . 9 ((𝜑𝑥𝑆) → (0..^𝑁) ⊆ ℕ0)
175172, 174fssresd 6758 . . . . . . . 8 ((𝜑𝑥𝑆) → ((coe1𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
176164, 165, 175elmapdd 8851 . . . . . . 7 ((𝜑𝑥𝑆) → ((coe1𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁)))
177169ffund 6720 . . . . . . . . 9 ((𝜑𝑥𝑆) → Fun (coe1𝑥))
178 fzofi 13963 . . . . . . . . . 10 (0..^𝑁) ∈ Fin
179178a1i 11 . . . . . . . . 9 ((𝜑𝑥𝑆) → (0..^𝑁) ∈ Fin)
180 fvexd 6906 . . . . . . . . 9 ((𝜑𝑥𝑆) → (0g‘(Scalar‘𝑃)) ∈ V)
181177, 179, 180resfifsupp 9412 . . . . . . . 8 ((𝜑𝑥𝑆) → ((coe1𝑥) ↾ (0..^𝑁)) finSupp (0g‘(Scalar‘𝑃)))
182 ringcmn 20207 . . . . . . . . . . . 12 (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
1836, 92, 1823syl 18 . . . . . . . . . . 11 (𝜑𝑃 ∈ CMnd)
184183adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝑃 ∈ CMnd)
185 nn0ex 12500 . . . . . . . . . . 11 0 ∈ V
186185a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝑆) → ℕ0 ∈ V)
18723ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑃 ∈ LMod)
188172ffvelcdmda 7088 . . . . . . . . . . . 12 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → ((coe1𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃)))
1896ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑅 ∈ Ring)
190189, 92, 933syl 18 . . . . . . . . . . . . 13 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → (mulGrp‘𝑃) ∈ Mnd)
191 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
192189, 99syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → (var1𝑅) ∈ (Base‘𝑃))
19390, 91, 190, 191, 192mulgnn0cld 19041 . . . . . . . . . . . 12 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝑃))
19433, 37, 38, 39, 187, 188, 193lmodvscld 20751 . . . . . . . . . . 11 (((𝜑𝑥𝑆) ∧ 𝑖 ∈ ℕ0) → (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))) ∈ (Base‘𝑃))
195 eqid 2727 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) = (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))
196194, 195fmptd 7118 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))):ℕ0⟶(Base‘𝑃))
197 nfv 1910 . . . . . . . . . . . 12 𝑖(𝜑𝑥𝑆)
198197, 194, 195fnmptd 6690 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) Fn ℕ0)
199 fveq2 6891 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → ((coe1𝑥)‘𝑖) = ((coe1𝑥)‘𝑗))
200 oveq1 7421 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑗(.g‘(mulGrp‘𝑃))(var1𝑅)))
201199, 200oveq12d 7432 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))) = (((coe1𝑥)‘𝑗)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))))
202 simplr 768 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → 𝑗 ∈ ℕ0)
203 ovexd 7449 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (((coe1𝑥)‘𝑗)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))) ∈ V)
204195, 201, 202, 203fvmptd3 7022 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))‘𝑗) = (((coe1𝑥)‘𝑗)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))))
205166ad2antrr 725 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → 𝑥 ∈ (Base‘𝑃))
206 icossxr 13433 . . . . . . . . . . . . . . . . 17 (-∞[,)𝑁) ⊆ ℝ*
207206, 75sselid 3976 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑆) → (𝐷𝑥) ∈ ℝ*)
208207ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (𝐷𝑥) ∈ ℝ*)
20954ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → 𝑁 ∈ ℝ*)
210202nn0red 12555 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → 𝑗 ∈ ℝ)
211210rexrd 11286 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → 𝑗 ∈ ℝ*)
21279ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (𝐷𝑥) < 𝑁)
213 simpr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → 𝑁𝑗)
214208, 209, 211, 212, 213xrltletrd 13164 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (𝐷𝑥) < 𝑗)
21524, 1, 33, 9, 167deg1lt 26020 . . . . . . . . . . . . . 14 ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ0 ∧ (𝐷𝑥) < 𝑗) → ((coe1𝑥)‘𝑗) = (0g𝑅))
216205, 202, 214, 215syl3anc 1369 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → ((coe1𝑥)‘𝑗) = (0g𝑅))
217216oveq1d 7429 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (((coe1𝑥)‘𝑗)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))) = ((0g𝑅)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))))
218147ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (0g𝑅) = (0g‘(Scalar‘𝑃)))
219218oveq1d 7429 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → ((0g𝑅)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))) = ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))))
22023ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → 𝑃 ∈ LMod)
22194ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (mulGrp‘𝑃) ∈ Mnd)
222100ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (var1𝑅) ∈ (Base‘𝑃))
22390, 91, 221, 202, 222mulgnn0cld 19041 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → (𝑗(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝑃))
224 eqid 2727 . . . . . . . . . . . . . . 15 (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
22533, 37, 38, 224, 10lmod0vs 20767 . . . . . . . . . . . . . 14 ((𝑃 ∈ LMod ∧ (𝑗(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝑃)) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))) = (0g𝑃))
226220, 223, 225syl2anc 583 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))) = (0g𝑃))
227219, 226eqtrd 2767 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → ((0g𝑅)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))) = (0g𝑃))
228204, 217, 2273eqtrd 2771 . . . . . . . . . . 11 ((((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁𝑗) → ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))‘𝑗) = (0g𝑃))
2293nn0zd 12606 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
230229adantr 480 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → 𝑁 ∈ ℤ)
231198, 228, 230suppssnn0 32558 . . . . . . . . . 10 ((𝜑𝑥𝑆) → ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) supp (0g𝑃)) ⊆ (0..^𝑁))
232186mptexd 7230 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ∈ V)
233198fnfund 6649 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → Fun (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))))
234 fvexd 6906 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (0g𝑃) ∈ V)
235 suppssfifsupp 9395 . . . . . . . . . . 11 ((((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ∈ V ∧ Fun (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ∧ (0g𝑃) ∈ V) ∧ ((0..^𝑁) ∈ Fin ∧ ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) supp (0g𝑃)) ⊆ (0..^𝑁))) → (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) finSupp (0g𝑃))
236232, 233, 234, 179, 231, 235syl32anc 1376 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) finSupp (0g𝑃))
23733, 10, 184, 186, 196, 231, 236gsumres 19859 . . . . . . . . 9 ((𝜑𝑥𝑆) → (𝑃 Σg ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σg (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))))
238 fvexd 6906 . . . . . . . . . . . 12 ((𝜑𝑥𝑆) → (coe1𝑥) ∈ V)
239 ovexd 7449 . . . . . . . . . . . . . 14 (𝜑 → (0..^𝑁) ∈ V)
240154, 239fexd 7233 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ V)
241240adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥𝑆) → 𝐹 ∈ V)
242 offres 7981 . . . . . . . . . . . 12 (((coe1𝑥) ∈ V ∧ 𝐹 ∈ V) → (((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹) ↾ (0..^𝑁)) = (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)(𝐹 ↾ (0..^𝑁))))
243238, 241, 242syl2anc 583 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹) ↾ (0..^𝑁)) = (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)(𝐹 ↾ (0..^𝑁))))
244169ffnd 6717 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑆) → (coe1𝑥) Fn ℕ0)
245154ffnd 6717 . . . . . . . . . . . . . . . 16 (𝜑𝐹 Fn (0..^𝑁))
246245adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑆) → 𝐹 Fn (0..^𝑁))
247 sseqin2 4211 . . . . . . . . . . . . . . . 16 ((0..^𝑁) ⊆ ℕ0 ↔ (ℕ0 ∩ (0..^𝑁)) = (0..^𝑁))
248173, 247mpbi 229 . . . . . . . . . . . . . . 15 (ℕ0 ∩ (0..^𝑁)) = (0..^𝑁)
249 eqidd 2728 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ ℕ0) → ((coe1𝑥)‘𝑗) = ((coe1𝑥)‘𝑗))
250 oveq1 7421 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑗 → (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑗(.g‘(mulGrp‘𝑃))(var1𝑅)))
251 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
252 ovexd 7449 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ V)
2538, 250, 251, 252fvmptd3 7022 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹𝑗) = (𝑗(.g‘(mulGrp‘𝑃))(var1𝑅)))
254244, 246, 186, 165, 248, 249, 253ofval 7690 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹)‘𝑗) = (((coe1𝑥)‘𝑗)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))))
255173, 251sselid 3976 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0)
256 ovexd 7449 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1𝑥)‘𝑗)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))) ∈ V)
257195, 201, 255, 256fvmptd3 7022 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))‘𝑗) = (((coe1𝑥)‘𝑗)( ·𝑠𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1𝑅))))
258254, 257eqtr4d 2770 . . . . . . . . . . . . 13 (((𝜑𝑥𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))‘𝑗))
259258ralrimiva 3141 . . . . . . . . . . . 12 ((𝜑𝑥𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))‘𝑗))
260244, 246, 186, 165, 248offn 7692 . . . . . . . . . . . . 13 ((𝜑𝑥𝑆) → ((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹) Fn (0..^𝑁))
261 ssidd 4001 . . . . . . . . . . . . 13 ((𝜑𝑥𝑆) → (0..^𝑁) ⊆ (0..^𝑁))
262 fvreseq0 7041 . . . . . . . . . . . . 13 (((((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹) Fn (0..^𝑁) ∧ (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) Fn ℕ0) ∧ ((0..^𝑁) ⊆ (0..^𝑁) ∧ (0..^𝑁) ⊆ ℕ0)) → ((((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))‘𝑗)))
263260, 198, 261, 174, 262syl22anc 838 . . . . . . . . . . . 12 ((𝜑𝑥𝑆) → ((((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))‘𝑗)))
264259, 263mpbird 257 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (((coe1𝑥) ∘f ( ·𝑠𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ↾ (0..^𝑁)))
265 fnresdm 6668 . . . . . . . . . . . . . 14 (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
266245, 265syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹)
267266adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
268267oveq2d 7430 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹))
269243, 264, 2683eqtr3rd 2776 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹) = ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ↾ (0..^𝑁)))
270269oveq2d 7430 . . . . . . . . 9 ((𝜑𝑥𝑆) → (𝑃 Σg (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹)) = (𝑃 Σg ((𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))) ↾ (0..^𝑁))))
2716adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝑅 ∈ Ring)
2721, 98, 33, 38, 89, 91, 167ply1coe 22204 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))))
273271, 166, 272syl2anc 583 . . . . . . . . 9 ((𝜑𝑥𝑆) → 𝑥 = (𝑃 Σg (𝑖 ∈ ℕ0 ↦ (((coe1𝑥)‘𝑖)( ·𝑠𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1𝑅))))))
274237, 270, 2733eqtr4rd 2778 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥 = (𝑃 Σg (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹)))
275181, 274jca 511 . . . . . . 7 ((𝜑𝑥𝑆) → (((coe1𝑥) ↾ (0..^𝑁)) finSupp (0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (((coe1𝑥) ↾ (0..^𝑁)) ∘f ( ·𝑠𝑃)𝐹))))
276163, 176, 275rspcedvdw 3610 . . . . . 6 ((𝜑𝑥𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))(𝑎 finSupp (0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹))))
277102, 8fmptd 7118 . . . . . . . 8 (𝜑𝐹:(0..^𝑁)⟶(Base‘𝑃))
278156, 33, 39, 37, 224, 38, 277, 23, 239ellspd 21723 . . . . . . 7 (𝜑 → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))(𝑎 finSupp (0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹)))))
279278adantr 480 . . . . . 6 ((𝜑𝑥𝑆) → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))(𝑎 finSupp (0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎f ( ·𝑠𝑃)𝐹)))))
280276, 279mpbird 257 . . . . 5 ((𝜑𝑥𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
281 imadmrn 6067 . . . . . . . 8 (𝐹 “ dom 𝐹) = ran 𝐹
282154fdmd 6727 . . . . . . . . 9 (𝜑 → dom 𝐹 = (0..^𝑁))
283282imaeq2d 6057 . . . . . . . 8 (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁)))
284281, 283eqtr3id 2781 . . . . . . 7 (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁)))
285284fveq2d 6895 . . . . . 6 (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
286285adantr 480 . . . . 5 ((𝜑𝑥𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
287280, 286eleqtrrd 2831 . . . 4 ((𝜑𝑥𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘ran 𝐹))
288158, 287eqelssd 3999 . . 3 (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆)
289 eqid 2727 . . . . . 6 (LSpan‘𝐸) = (LSpan‘𝐸)
29044, 156, 289, 27lsslsp 20888 . . . . 5 ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹))
291290eqcomd 2733 . . . 4 ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
29223, 26, 155, 291syl3anc 1369 . . 3 (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
293288, 292, 463eqtr3d 2775 . 2 (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))
294 eqid 2727 . . 3 (Base‘𝐸) = (Base‘𝐸)
29524fvexi 6905 . . . . . . 7 𝐷 ∈ V
296 cnvexg 7926 . . . . . . 7 (𝐷 ∈ V → 𝐷 ∈ V)
297 imaexg 7915 . . . . . . 7 (𝐷 ∈ V → (𝐷 “ (-∞[,)𝑁)) ∈ V)
298295, 296, 297mp2b 10 . . . . . 6 (𝐷 “ (-∞[,)𝑁)) ∈ V
29925, 298eqeltri 2824 . . . . 5 𝑆 ∈ V
30044, 37resssca 17315 . . . . 5 (𝑆 ∈ V → (Scalar‘𝑃) = (Scalar‘𝐸))
301299, 300ax-mp 5 . . . 4 (Scalar‘𝑃) = (Scalar‘𝐸)
302301fveq2i 6894 . . 3 (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸))
303 eqid 2727 . . 3 (Scalar‘𝐸) = (Scalar‘𝐸)
30444, 38ressvsca 17316 . . . 4 (𝑆 ∈ V → ( ·𝑠𝑃) = ( ·𝑠𝐸))
305299, 304ax-mp 5 . . 3 ( ·𝑠𝑃) = ( ·𝑠𝐸)
306 eqid 2727 . . 3 (0g𝐸) = (0g𝐸)
307301fveq2i 6894 . . 3 (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝐸))
308 eqid 2727 . . 3 (LBasis‘𝐸) = (LBasis‘𝐸)
30944, 27lsslvec 20983 . . . . 5 ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec)
31022, 26, 309syl2anc 583 . . . 4 (𝜑𝐸 ∈ LVec)
311310lveclmodd 20981 . . 3 (𝜑𝐸 ∈ LMod)
31214, 5eqeltrrd 2829 . . . . 5 (𝜑 → (Scalar‘𝑃) ∈ DivRing)
313 drngnzr 20633 . . . . 5 ((Scalar‘𝑃) ∈ DivRing → (Scalar‘𝑃) ∈ NzRing)
314312, 313syl 17 . . . 4 (𝜑 → (Scalar‘𝑃) ∈ NzRing)
315301, 314eqeltrrid 2833 . . 3 (𝜑 → (Scalar‘𝐸) ∈ NzRing)
316120ralrimiva 3141 . . . 4 (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝐸))
317 drngnzr 20633 . . . . . . . . . 10 (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
3185, 317syl 17 . . . . . . . . 9 (𝜑𝑅 ∈ NzRing)
319318ad2antrr 725 . . . . . . . 8 (((𝜑𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing)
32097adantr 480 . . . . . . . 8 (((𝜑𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ0)
321 elfzonn0 13701 . . . . . . . . 9 (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ0)
322321adantl 481 . . . . . . . 8 (((𝜑𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ0)
3231, 98, 91, 319, 320, 322ply1moneq 33196 . . . . . . 7 (((𝜑𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)) ↔ 𝑛 = 𝑖))
324323biimpd 228 . . . . . 6 (((𝜑𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)) → 𝑛 = 𝑖))
325324anasss 466 . . . . 5 ((𝜑 ∧ (𝑛 ∈ (0..^𝑁) ∧ 𝑖 ∈ (0..^𝑁))) → ((𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)) → 𝑛 = 𝑖))
326325ralrimivva 3195 . . . 4 (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)) → 𝑛 = 𝑖))
327 oveq1 7421 . . . . 5 (𝑛 = 𝑖 → (𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)))
3288, 327f1mpt 7265 . . . 4 (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1𝑅)) → 𝑛 = 𝑖)))
329316, 326, 328sylanbrc 582 . . 3 (𝜑𝐹:(0..^𝑁)–1-1→(Base‘𝐸))
330294, 302, 303, 305, 306, 307, 308, 289, 311, 315, 239, 329islbs5 33035 . 2 (𝜑 → (ran 𝐹 ∈ (LBasis‘𝐸) ↔ (∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))((𝑎 finSupp (0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎f ( ·𝑠𝑃)𝐹)) = (0g𝐸)) → 𝑎 = ((0..^𝑁) × {(0g‘(Scalar‘𝑃))})) ∧ ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))))
331153, 293, 330mpbir2and 712 1 (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wral 3056  wrex 3065  Vcvv 3469  cin 3943  wss 3944  {csn 4624   class class class wbr 5142  cmpt 5225   × cxp 5670  ccnv 5671  dom cdm 5672  ran crn 5673  cres 5674  cima 5675  Fun wfun 6536   Fn wfn 6537  wf 6538  1-1wf1 6539  cfv 6542  (class class class)co 7414  f cof 7677   supp csupp 8159  m cmap 8836  Fincfn 8955   finSupp cfsupp 9377  0cc0 11130  -∞cmnf 11268  *cxr 11269   < clt 11270  cle 11271  0cn0 12494  cz 12580  [,)cico 13350  ..^cfzo 13651  Basecbs 17171  s cress 17200  Scalarcsca 17227   ·𝑠 cvsca 17228  0gc0g 17412   Σg cgsu 17413  Mndcmnd 18685  SubMndcsubmnd 18730  .gcmg 19014  SubGrpcsubg 19066  CMndccmn 19726  mulGrpcmgp 20065  Ringcrg 20164  NzRingcnzr 20440  DivRingcdr 20613  LModclmod 20732  LSubSpclss 20804  LSpanclspn 20844  LBasisclbs 20948  LVecclvec 20976  var1cv1 22082  Poly1cpl1 22083  coe1cco1 22084   deg1 cdg1 25974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-ofr 7680  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-tpos 8225  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-sup 9457  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-ico 13354  df-fz 13509  df-fzo 13652  df-seq 13991  df-hash 14314  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-0g 17414  df-gsum 17415  df-prds 17420  df-pws 17422  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-mhm 18731  df-submnd 18732  df-grp 18884  df-minusg 18885  df-sbg 18886  df-mulg 19015  df-subg 19069  df-ghm 19159  df-cntz 19259  df-cmn 19728  df-abl 19729  df-mgp 20066  df-rng 20084  df-ur 20113  df-srg 20118  df-ring 20166  df-cring 20167  df-oppr 20262  df-dvdsr 20285  df-unit 20286  df-nzr 20441  df-subrng 20472  df-subrg 20497  df-drng 20615  df-lmod 20734  df-lss 20805  df-lsp 20845  df-lmhm 20896  df-lbs 20949  df-lvec 20977  df-sra 21047  df-rgmod 21048  df-cnfld 21267  df-dsmm 21653  df-frlm 21668  df-uvc 21704  df-lindf 21727  df-linds 21728  df-psr 21829  df-mvr 21830  df-mpl 21831  df-opsr 21833  df-psr1 22086  df-vr1 22087  df-ply1 22088  df-coe1 22089  df-mdeg 25975  df-deg1 25976
This theorem is referenced by:  ply1degltdim  33253
  Copyright terms: Public domain W3C validator