Metamath Proof Explorer


Theorem lindspropd

Description: Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023)

Ref Expression
Hypotheses lindfpropd.1 φ Base K = Base L
lindfpropd.2 φ Base Scalar K = Base Scalar L
lindfpropd.3 φ 0 Scalar K = 0 Scalar L
lindfpropd.4 φ x Base K y Base K x + K y = x + L y
lindfpropd.5 φ x Base Scalar K y Base K x K y Base K
lindfpropd.6 φ x Base Scalar K y Base K x K y = x L y
lindfpropd.k φ K V
lindfpropd.l φ L W
Assertion lindspropd φ LIndS K = LIndS L

Proof

Step Hyp Ref Expression
1 lindfpropd.1 φ Base K = Base L
2 lindfpropd.2 φ Base Scalar K = Base Scalar L
3 lindfpropd.3 φ 0 Scalar K = 0 Scalar L
4 lindfpropd.4 φ x Base K y Base K x + K y = x + L y
5 lindfpropd.5 φ x Base Scalar K y Base K x K y Base K
6 lindfpropd.6 φ x Base Scalar K y Base K x K y = x L y
7 lindfpropd.k φ K V
8 lindfpropd.l φ L W
9 1 sseq2d φ z Base K z Base L
10 vex z V
11 10 a1i φ z V
12 11 resiexd φ I z V
13 1 2 3 4 5 6 7 8 12 lindfpropd φ I z LIndF K I z LIndF L
14 9 13 anbi12d φ z Base K I z LIndF K z Base L I z LIndF L
15 eqid Base K = Base K
16 15 islinds K V z LIndS K z Base K I z LIndF K
17 7 16 syl φ z LIndS K z Base K I z LIndF K
18 eqid Base L = Base L
19 18 islinds L W z LIndS L z Base L I z LIndF L
20 8 19 syl φ z LIndS L z Base L I z LIndF L
21 14 17 20 3bitr4d φ z LIndS K z LIndS L
22 21 eqrdv φ LIndS K = LIndS L