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 ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
lindfpropd.2 ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
lindfpropd.3 ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
lindfpropd.4 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
lindfpropd.5 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
lindfpropd.6 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝐿 ) 𝑦 ) )
lindfpropd.k ( 𝜑𝐾𝑉 )
lindfpropd.l ( 𝜑𝐿𝑊 )
Assertion lindspropd ( 𝜑 → ( LIndS ‘ 𝐾 ) = ( LIndS ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 lindfpropd.1 ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
2 lindfpropd.2 ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
3 lindfpropd.3 ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
4 lindfpropd.4 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
5 lindfpropd.5 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
6 lindfpropd.6 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝐿 ) 𝑦 ) )
7 lindfpropd.k ( 𝜑𝐾𝑉 )
8 lindfpropd.l ( 𝜑𝐿𝑊 )
9 1 sseq2d ( 𝜑 → ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ↔ 𝑧 ⊆ ( Base ‘ 𝐿 ) ) )
10 vex 𝑧 ∈ V
11 10 a1i ( 𝜑𝑧 ∈ V )
12 11 resiexd ( 𝜑 → ( I ↾ 𝑧 ) ∈ V )
13 1 2 3 4 5 6 7 8 12 lindfpropd ( 𝜑 → ( ( I ↾ 𝑧 ) LIndF 𝐾 ↔ ( I ↾ 𝑧 ) LIndF 𝐿 ) )
14 9 13 anbi12d ( 𝜑 → ( ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( I ↾ 𝑧 ) LIndF 𝐾 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( I ↾ 𝑧 ) LIndF 𝐿 ) ) )
15 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16 15 islinds ( 𝐾𝑉 → ( 𝑧 ∈ ( LIndS ‘ 𝐾 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( I ↾ 𝑧 ) LIndF 𝐾 ) ) )
17 7 16 syl ( 𝜑 → ( 𝑧 ∈ ( LIndS ‘ 𝐾 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( I ↾ 𝑧 ) LIndF 𝐾 ) ) )
18 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
19 18 islinds ( 𝐿𝑊 → ( 𝑧 ∈ ( LIndS ‘ 𝐿 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( I ↾ 𝑧 ) LIndF 𝐿 ) ) )
20 8 19 syl ( 𝜑 → ( 𝑧 ∈ ( LIndS ‘ 𝐿 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( I ↾ 𝑧 ) LIndF 𝐿 ) ) )
21 14 17 20 3bitr4d ( 𝜑 → ( 𝑧 ∈ ( LIndS ‘ 𝐾 ) ↔ 𝑧 ∈ ( LIndS ‘ 𝐿 ) ) )
22 21 eqrdv ( 𝜑 → ( LIndS ‘ 𝐾 ) = ( LIndS ‘ 𝐿 ) )