This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐿 ) )