Metamath Proof Explorer


Theorem lindspropd

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

Ref Expression
Hypotheses lindfpropd.1 φBaseK=BaseL
lindfpropd.2 φBaseScalarK=BaseScalarL
lindfpropd.3 φ0ScalarK=0ScalarL
lindfpropd.4 φxBaseKyBaseKx+Ky=x+Ly
lindfpropd.5 φxBaseScalarKyBaseKxKyBaseK
lindfpropd.6 φxBaseScalarKyBaseKxKy=xLy
lindfpropd.k φKV
lindfpropd.l φLW
Assertion lindspropd φLIndSK=LIndSL

Proof

Step Hyp Ref Expression
1 lindfpropd.1 φBaseK=BaseL
2 lindfpropd.2 φBaseScalarK=BaseScalarL
3 lindfpropd.3 φ0ScalarK=0ScalarL
4 lindfpropd.4 φxBaseKyBaseKx+Ky=x+Ly
5 lindfpropd.5 φxBaseScalarKyBaseKxKyBaseK
6 lindfpropd.6 φxBaseScalarKyBaseKxKy=xLy
7 lindfpropd.k φKV
8 lindfpropd.l φLW
9 1 sseq2d φzBaseKzBaseL
10 vex zV
11 10 a1i φzV
12 11 resiexd φIzV
13 1 2 3 4 5 6 7 8 12 lindfpropd φIzLIndFKIzLIndFL
14 9 13 anbi12d φzBaseKIzLIndFKzBaseLIzLIndFL
15 eqid BaseK=BaseK
16 15 islinds KVzLIndSKzBaseKIzLIndFK
17 7 16 syl φzLIndSKzBaseKIzLIndFK
18 eqid BaseL=BaseL
19 18 islinds LWzLIndSLzBaseLIzLIndFL
20 8 19 syl φzLIndSLzBaseLIzLIndFL
21 14 17 20 3bitr4d φzLIndSKzLIndSL
22 21 eqrdv φLIndSK=LIndSL