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 ⊢φ→B=BaseK
lsspropd.b2 ⊢φ→B=BaseL
lsspropd.w ⊢φ→B⊆W
lsspropd.p ⊢φ∧x∈W∧y∈W→x+Ky=x+Ly
lsspropd.s1 ⊢φ∧x∈P∧y∈B→x⋅Ky∈W
lsspropd.s2 ⊢φ∧x∈P∧y∈B→x⋅Ky=x⋅Ly
lsspropd.p1 ⊢φ→P=BaseScalar⁡K
lsspropd.p2 ⊢φ→P=BaseScalar⁡L
Assertion lsspropd ⊢φ→LSubSp⁡K=LSubSp⁡L

Proof

Step Hyp Ref Expression
1 lsspropd.b1 ⊢φ→B=BaseK
2 lsspropd.b2 ⊢φ→B=BaseL
3 lsspropd.w ⊢φ→B⊆W
4 lsspropd.p ⊢φ∧x∈W∧y∈W→x+Ky=x+Ly
5 lsspropd.s1 ⊢φ∧x∈P∧y∈B→x⋅Ky∈W
6 lsspropd.s2 ⊢φ∧x∈P∧y∈B→x⋅Ky=x⋅Ly
7 lsspropd.p1 ⊢φ→P=BaseScalar⁡K
8 lsspropd.p2 ⊢φ→P=BaseScalar⁡L
9 simpll ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→φ
10 simprl ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z∈P
11 simplr ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→s⊆B
12 simprrl ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→a∈s
13 11 12 sseldd ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→a∈B
14 5 ralrimivva ⊢φ→∀x∈P∀y∈Bx⋅Ky∈W
15 14 ad2antrr ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→∀x∈P∀y∈Bx⋅Ky∈W
16 ovrspc2v ⊢z∈P∧a∈B∧∀x∈P∀y∈Bx⋅Ky∈W→z⋅Ka∈W
17 10 13 15 16 syl21anc ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z⋅Ka∈W
18 3 ad2antrr ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→B⊆W
19 simprrr ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→b∈s
20 11 19 sseldd ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→b∈B
21 18 20 sseldd ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→b∈W
22 4 oveqrspc2v ⊢φ∧z⋅Ka∈W∧b∈W→z⋅Ka+Kb=z⋅Ka+Lb
23 9 17 21 22 syl12anc ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z⋅Ka+Kb=z⋅Ka+Lb
24 6 oveqrspc2v ⊢φ∧z∈P∧a∈B→z⋅Ka=z⋅La
25 9 10 13 24 syl12anc ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z⋅Ka=z⋅La
26 25 oveq1d ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z⋅Ka+Lb=z⋅La+Lb
27 23 26 eqtrd ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z⋅Ka+Kb=z⋅La+Lb
28 27 eleq1d ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z⋅Ka+Kb∈s↔z⋅La+Lb∈s
29 28 anassrs ⊢φ∧s⊆B∧z∈P∧a∈s∧b∈s→z⋅Ka+Kb∈s↔z⋅La+Lb∈s
30 29 2ralbidva ⊢φ∧s⊆B∧z∈P→∀a∈s∀b∈sz⋅Ka+Kb∈s↔∀a∈s∀b∈sz⋅La+Lb∈s
31 30 ralbidva ⊢φ∧s⊆B→∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s↔∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s
32 31 anbi2d ⊢φ∧s⊆B→s≠∅∧∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s↔s≠∅∧∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s
33 32 pm5.32da ⊢φ→s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s↔s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s
34 3anass ⊢s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s↔s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s
35 3anass ⊢s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s↔s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s
36 33 34 35 3bitr4g ⊢φ→s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s↔s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s
37 1 sseq2d ⊢φ→s⊆B↔s⊆BaseK
38 7 raleqdv ⊢φ→∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s↔∀z∈BaseScalar⁡K∀a∈s∀b∈sz⋅Ka+Kb∈s
39 37 38 3anbi13d ⊢φ→s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅Ka+Kb∈s↔s⊆BaseK∧s≠∅∧∀z∈BaseScalar⁡K∀a∈s∀b∈sz⋅Ka+Kb∈s
40 2 sseq2d ⊢φ→s⊆B↔s⊆BaseL
41 8 raleqdv ⊢φ→∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s↔∀z∈BaseScalar⁡L∀a∈s∀b∈sz⋅La+Lb∈s
42 40 41 3anbi13d ⊢φ→s⊆B∧s≠∅∧∀z∈P∀a∈s∀b∈sz⋅La+Lb∈s↔s⊆BaseL∧s≠∅∧∀z∈BaseScalar⁡L∀a∈s∀b∈sz⋅La+Lb∈s
43 36 39 42 3bitr3d ⊢φ→s⊆BaseK∧s≠∅∧∀z∈BaseScalar⁡K∀a∈s∀b∈sz⋅Ka+Kb∈s↔s⊆BaseL∧s≠∅∧∀z∈BaseScalar⁡L∀a∈s∀b∈sz⋅La+Lb∈s
44 eqid ⊢Scalar⁡K=Scalar⁡K
45 eqid ⊢BaseScalar⁡K=BaseScalar⁡K
46 eqid ⊢BaseK=BaseK
47 eqid ⊢+K=+K
48 eqid ⊢⋅K=⋅K
49 eqid ⊢LSubSp⁡K=LSubSp⁡K
50 44 45 46 47 48 49 islss ⊢s∈LSubSp⁡K↔s⊆BaseK∧s≠∅∧∀z∈BaseScalar⁡K∀a∈s∀b∈sz⋅Ka+Kb∈s
51 eqid ⊢Scalar⁡L=Scalar⁡L
52 eqid ⊢BaseScalar⁡L=BaseScalar⁡L
53 eqid ⊢BaseL=BaseL
54 eqid ⊢+L=+L
55 eqid ⊢⋅L=⋅L
56 eqid ⊢LSubSp⁡L=LSubSp⁡L
57 51 52 53 54 55 56 islss ⊢s∈LSubSp⁡L↔s⊆BaseL∧s≠∅∧∀z∈BaseScalar⁡L∀a∈s∀b∈sz⋅La+Lb∈s
58 43 50 57 3bitr4g ⊢φ→s∈LSubSp⁡K↔s∈LSubSp⁡L
59 58 eqrdv ⊢φ→LSubSp⁡K=LSubSp⁡L