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