Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  islininds Structured version   Visualization version   GIF version

Theorem islininds 47080
Description: The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.)
Hypotheses
Ref Expression
islininds.b 𝐡 = (Baseβ€˜π‘€)
islininds.z 𝑍 = (0gβ€˜π‘€)
islininds.r 𝑅 = (Scalarβ€˜π‘€)
islininds.e 𝐸 = (Baseβ€˜π‘…)
islininds.0 0 = (0gβ€˜π‘…)
Assertion
Ref Expression
islininds ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ π‘Š) β†’ (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐡 ∧ βˆ€π‘“ ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))))
Distinct variable groups:   𝑓,𝐸   𝑓,𝑀,π‘₯   𝑆,𝑓,π‘₯
Allowed substitution hints:   𝐡(π‘₯,𝑓)   𝑅(π‘₯,𝑓)   𝐸(π‘₯)   𝑉(π‘₯,𝑓)   π‘Š(π‘₯,𝑓)   0 (π‘₯,𝑓)   𝑍(π‘₯,𝑓)

Proof of Theorem islininds
Dummy variables π‘š 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 483 . . . 4 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ 𝑠 = 𝑆)
2 fveq2 6888 . . . . . . 7 (π‘š = 𝑀 β†’ (Baseβ€˜π‘š) = (Baseβ€˜π‘€))
3 islininds.b . . . . . . 7 𝐡 = (Baseβ€˜π‘€)
42, 3eqtr4di 2790 . . . . . 6 (π‘š = 𝑀 β†’ (Baseβ€˜π‘š) = 𝐡)
54adantl 482 . . . . 5 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (Baseβ€˜π‘š) = 𝐡)
65pweqd 4618 . . . 4 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ 𝒫 (Baseβ€˜π‘š) = 𝒫 𝐡)
71, 6eleq12d 2827 . . 3 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (𝑠 ∈ 𝒫 (Baseβ€˜π‘š) ↔ 𝑆 ∈ 𝒫 𝐡))
8 fveq2 6888 . . . . . . . . 9 (π‘š = 𝑀 β†’ (Scalarβ€˜π‘š) = (Scalarβ€˜π‘€))
9 islininds.r . . . . . . . . 9 𝑅 = (Scalarβ€˜π‘€)
108, 9eqtr4di 2790 . . . . . . . 8 (π‘š = 𝑀 β†’ (Scalarβ€˜π‘š) = 𝑅)
1110fveq2d 6892 . . . . . . 7 (π‘š = 𝑀 β†’ (Baseβ€˜(Scalarβ€˜π‘š)) = (Baseβ€˜π‘…))
12 islininds.e . . . . . . 7 𝐸 = (Baseβ€˜π‘…)
1311, 12eqtr4di 2790 . . . . . 6 (π‘š = 𝑀 β†’ (Baseβ€˜(Scalarβ€˜π‘š)) = 𝐸)
1413adantl 482 . . . . 5 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (Baseβ€˜(Scalarβ€˜π‘š)) = 𝐸)
1514, 1oveq12d 7423 . . . 4 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ((Baseβ€˜(Scalarβ€˜π‘š)) ↑m 𝑠) = (𝐸 ↑m 𝑆))
168adantl 482 . . . . . . . . . 10 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (Scalarβ€˜π‘š) = (Scalarβ€˜π‘€))
1716, 9eqtr4di 2790 . . . . . . . . 9 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (Scalarβ€˜π‘š) = 𝑅)
1817fveq2d 6892 . . . . . . . 8 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (0gβ€˜(Scalarβ€˜π‘š)) = (0gβ€˜π‘…))
19 islininds.0 . . . . . . . 8 0 = (0gβ€˜π‘…)
2018, 19eqtr4di 2790 . . . . . . 7 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (0gβ€˜(Scalarβ€˜π‘š)) = 0 )
2120breq2d 5159 . . . . . 6 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (𝑓 finSupp (0gβ€˜(Scalarβ€˜π‘š)) ↔ 𝑓 finSupp 0 ))
22 fveq2 6888 . . . . . . . . 9 (π‘š = 𝑀 β†’ ( linC β€˜π‘š) = ( linC β€˜π‘€))
2322adantl 482 . . . . . . . 8 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ( linC β€˜π‘š) = ( linC β€˜π‘€))
24 eqidd 2733 . . . . . . . 8 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ 𝑓 = 𝑓)
2523, 24, 1oveq123d 7426 . . . . . . 7 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (𝑓( linC β€˜π‘š)𝑠) = (𝑓( linC β€˜π‘€)𝑆))
26 fveq2 6888 . . . . . . . . 9 (π‘š = 𝑀 β†’ (0gβ€˜π‘š) = (0gβ€˜π‘€))
2726adantl 482 . . . . . . . 8 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (0gβ€˜π‘š) = (0gβ€˜π‘€))
28 islininds.z . . . . . . . 8 𝑍 = (0gβ€˜π‘€)
2927, 28eqtr4di 2790 . . . . . . 7 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (0gβ€˜π‘š) = 𝑍)
3025, 29eqeq12d 2748 . . . . . 6 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ((𝑓( linC β€˜π‘š)𝑠) = (0gβ€˜π‘š) ↔ (𝑓( linC β€˜π‘€)𝑆) = 𝑍))
3121, 30anbi12d 631 . . . . 5 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ((𝑓 finSupp (0gβ€˜(Scalarβ€˜π‘š)) ∧ (𝑓( linC β€˜π‘š)𝑠) = (0gβ€˜π‘š)) ↔ (𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍)))
3210fveq2d 6892 . . . . . . . . 9 (π‘š = 𝑀 β†’ (0gβ€˜(Scalarβ€˜π‘š)) = (0gβ€˜π‘…))
3332, 19eqtr4di 2790 . . . . . . . 8 (π‘š = 𝑀 β†’ (0gβ€˜(Scalarβ€˜π‘š)) = 0 )
3433adantl 482 . . . . . . 7 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (0gβ€˜(Scalarβ€˜π‘š)) = 0 )
3534eqeq2d 2743 . . . . . 6 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ((π‘“β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘š)) ↔ (π‘“β€˜π‘₯) = 0 ))
361, 35raleqbidv 3342 . . . . 5 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (βˆ€π‘₯ ∈ 𝑠 (π‘“β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘š)) ↔ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))
3731, 36imbi12d 344 . . . 4 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (((𝑓 finSupp (0gβ€˜(Scalarβ€˜π‘š)) ∧ (𝑓( linC β€˜π‘š)𝑠) = (0gβ€˜π‘š)) β†’ βˆ€π‘₯ ∈ 𝑠 (π‘“β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘š))) ↔ ((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 )))
3815, 37raleqbidv 3342 . . 3 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (βˆ€π‘“ ∈ ((Baseβ€˜(Scalarβ€˜π‘š)) ↑m 𝑠)((𝑓 finSupp (0gβ€˜(Scalarβ€˜π‘š)) ∧ (𝑓( linC β€˜π‘š)𝑠) = (0gβ€˜π‘š)) β†’ βˆ€π‘₯ ∈ 𝑠 (π‘“β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘š))) ↔ βˆ€π‘“ ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 )))
397, 38anbi12d 631 . 2 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ((𝑠 ∈ 𝒫 (Baseβ€˜π‘š) ∧ βˆ€π‘“ ∈ ((Baseβ€˜(Scalarβ€˜π‘š)) ↑m 𝑠)((𝑓 finSupp (0gβ€˜(Scalarβ€˜π‘š)) ∧ (𝑓( linC β€˜π‘š)𝑠) = (0gβ€˜π‘š)) β†’ βˆ€π‘₯ ∈ 𝑠 (π‘“β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘š)))) ↔ (𝑆 ∈ 𝒫 𝐡 ∧ βˆ€π‘“ ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))))
40 df-lininds 47076 . 2 linIndS = {βŸ¨π‘ , π‘šβŸ© ∣ (𝑠 ∈ 𝒫 (Baseβ€˜π‘š) ∧ βˆ€π‘“ ∈ ((Baseβ€˜(Scalarβ€˜π‘š)) ↑m 𝑠)((𝑓 finSupp (0gβ€˜(Scalarβ€˜π‘š)) ∧ (𝑓( linC β€˜π‘š)𝑠) = (0gβ€˜π‘š)) β†’ βˆ€π‘₯ ∈ 𝑠 (π‘“β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘š))))}
4139, 40brabga 5533 1 ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ π‘Š) β†’ (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐡 ∧ βˆ€π‘“ ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  π’« cpw 4601   class class class wbr 5147  β€˜cfv 6540  (class class class)co 7405   ↑m cmap 8816   finSupp cfsupp 9357  Basecbs 17140  Scalarcsca 17196  0gc0g 17381   linC clinc 47038   linIndS clininds 47074
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-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-iota 6492  df-fv 6548  df-ov 7408  df-lininds 47076
This theorem is referenced by:  linindsi  47081  islinindfis  47083  islindeps  47087  lindslininds  47098  linds0  47099  lindsrng01  47102  snlindsntor  47105
  Copyright terms: Public domain W3C validator