Step 
Hyp 
Ref 
Expression 
1 

ocv2ss.o 
⊢ ⊥ = ( ocv ‘ 𝑊 ) 
2 

sstr2 
⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑆 ⊆ ( Base ‘ 𝑊 ) → 𝑇 ⊆ ( Base ‘ 𝑊 ) ) ) 
3 

idd 
⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑥 ∈ ( Base ‘ 𝑊 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) ) ) 
4 

ssralv 
⊢ ( 𝑇 ⊆ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·_{𝑖} ‘ 𝑊 ) 𝑦 ) = ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) → ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( ·_{𝑖} ‘ 𝑊 ) 𝑦 ) = ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) ) ) 
5 
2 3 4

3anim123d 
⊢ ( 𝑇 ⊆ 𝑆 → ( ( 𝑆 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·_{𝑖} ‘ 𝑊 ) 𝑦 ) = ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑇 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( ·_{𝑖} ‘ 𝑊 ) 𝑦 ) = ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) ) ) ) 
6 

eqid 
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) 
7 

eqid 
⊢ ( ·_{𝑖} ‘ 𝑊 ) = ( ·_{𝑖} ‘ 𝑊 ) 
8 

eqid 
⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) 
9 

eqid 
⊢ ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) = ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) 
10 
6 7 8 9 1

elocv 
⊢ ( 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·_{𝑖} ‘ 𝑊 ) 𝑦 ) = ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) ) ) 
11 
6 7 8 9 1

elocv 
⊢ ( 𝑥 ∈ ( ⊥ ‘ 𝑇 ) ↔ ( 𝑇 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( ·_{𝑖} ‘ 𝑊 ) 𝑦 ) = ( 0_{g} ‘ ( Scalar ‘ 𝑊 ) ) ) ) 
12 
5 10 11

3imtr4g 
⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑥 ∈ ( ⊥ ‘ 𝑆 ) → 𝑥 ∈ ( ⊥ ‘ 𝑇 ) ) ) 
13 
12

ssrdv 
⊢ ( 𝑇 ⊆ 𝑆 → ( ⊥ ‘ 𝑆 ) ⊆ ( ⊥ ‘ 𝑇 ) ) 