Metamath Proof Explorer

Theorem lsspropd

Description: If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses lsspropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
lsspropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
lsspropd.w ⊢ ( 𝜑 → 𝐵 ⊆ 𝑊 )
lsspropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lsspropd.s1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
lsspropd.s2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
lsspropd.p1 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
lsspropd.p2 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
Assertion lsspropd ( 𝜑 → ( LSubSp ‘ 𝐾 ) = ( LSubSp ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 lsspropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lsspropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 lsspropd.w ⊢ ( 𝜑 → 𝐵 ⊆ 𝑊 )
4 lsspropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
5 lsspropd.s1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
6 lsspropd.s2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
7 lsspropd.p1 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
8 lsspropd.p2 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
9 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝜑 )
10 simprl ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝑧 ∈ 𝑃 )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝑠 ⊆ 𝐵 )
12 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝑎 ∈ 𝑠 )
13 11 12 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝑎 ∈ 𝐵 )
14 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
16 ovrspc2v ⊢ ( ( ( 𝑧 ∈ 𝑃 ∧ 𝑎 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 ) → ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ∈ 𝑊 )
17 10 13 15 16 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ∈ 𝑊 )
18 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝐵 ⊆ 𝑊 )
19 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝑏 ∈ 𝑠 )
20 11 19 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝑏 ∈ 𝐵 )
21 18 20 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → 𝑏 ∈ 𝑊 )
22 4 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) = ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) )
23 9 17 21 22 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) = ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) )
24 6 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑎 ∈ 𝐵 ) ) → ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) = ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) )
25 9 10 13 24 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) = ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) )
26 25 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) = ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) )
27 23 26 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) = ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) )
28 27 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ 𝑃 ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) ) → ( ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ↔ ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) )
29 28 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠 ) ) → ( ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ↔ ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) )
30 29 2ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝑃 ) → ( ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) )
31 30 ralbidva ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) )
32 31 anbi2d ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → ( ( 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ↔ ( 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ) )
33 32 pm5.32da ⊢ ( 𝜑 → ( ( 𝑠 ⊆ 𝐵 ∧ ( 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ) ↔ ( 𝑠 ⊆ 𝐵 ∧ ( 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ) ) )
34 3anass ⊢ ( ( 𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ 𝐵 ∧ ( 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ) )
35 3anass ⊢ ( ( 𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ 𝐵 ∧ ( 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ) )
36 33 34 35 3bitr4g ⊢ ( 𝜑 → ( ( 𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ) )
37 1 sseq2d ⊢ ( 𝜑 → ( 𝑠 ⊆ 𝐵 ↔ 𝑠 ⊆ ( Base ‘ 𝐾 ) ) )
38 7 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) )
39 37 38 3anbi13d ⊢ ( 𝜑 → ( ( 𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ) )
40 2 sseq2d ⊢ ( 𝜑 → ( 𝑠 ⊆ 𝐵 ↔ 𝑠 ⊆ ( Base ‘ 𝐿 ) ) )
41 8 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) )
42 40 41 3anbi13d ⊢ ( 𝜑 → ( ( 𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ ( Base ‘ 𝐿 ) ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ) )
43 36 39 42 3bitr3d ⊢ ( 𝜑 → ( ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ ( Base ‘ 𝐿 ) ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) ) )
44 eqid ⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
45 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐾 ) )
46 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
47 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
48 eqid ⊢ ( ·𝑠 ‘ 𝐾 ) = ( ·𝑠 ‘ 𝐾 )
49 eqid ⊢ ( LSubSp ‘ 𝐾 ) = ( LSubSp ‘ 𝐾 )
50 44 45 46 47 48 49 islss ⊢ ( 𝑠 ∈ ( LSubSp ‘ 𝐾 ) ↔ ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐾 ) 𝑎 ) ( +g ‘ 𝐾 ) 𝑏 ) ∈ 𝑠 ) )
51 eqid ⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
52 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐿 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) )
53 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
54 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
55 eqid ⊢ ( ·𝑠 ‘ 𝐿 ) = ( ·𝑠 ‘ 𝐿 )
56 eqid ⊢ ( LSubSp ‘ 𝐿 ) = ( LSubSp ‘ 𝐿 )
57 51 52 53 54 55 56 islss ⊢ ( 𝑠 ∈ ( LSubSp ‘ 𝐿 ) ↔ ( 𝑠 ⊆ ( Base ‘ 𝐿 ) ∧ 𝑠 ≠ ∅ ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑎 ) ( +g ‘ 𝐿 ) 𝑏 ) ∈ 𝑠 ) )
58 43 50 57 3bitr4g ⊢ ( 𝜑 → ( 𝑠 ∈ ( LSubSp ‘ 𝐾 ) ↔ 𝑠 ∈ ( LSubSp ‘ 𝐿 ) ) )
59 58 eqrdv ⊢ ( 𝜑 → ( LSubSp ‘ 𝐾 ) = ( LSubSp ‘ 𝐿 ) )