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