ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lsspropdg GIF version

Theorem lsspropdg 13615
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.)
Hypotheses
Ref Expression
lsspropd.b1 (𝜑𝐵 = (Base‘𝐾))
lsspropd.b2 (𝜑𝐵 = (Base‘𝐿))
lsspropd.w (𝜑𝐵𝑊)
lsspropd.p ((𝜑 ∧ (𝑥𝑊𝑦𝑊)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
lsspropd.s1 ((𝜑 ∧ (𝑥𝑃𝑦𝐵)) → (𝑥( ·𝑠𝐾)𝑦) ∈ 𝑊)
lsspropd.s2 ((𝜑 ∧ (𝑥𝑃𝑦𝐵)) → (𝑥( ·𝑠𝐾)𝑦) = (𝑥( ·𝑠𝐿)𝑦))
lsspropd.p1 (𝜑𝑃 = (Base‘(Scalar‘𝐾)))
lsspropd.p2 (𝜑𝑃 = (Base‘(Scalar‘𝐿)))
lsppropd.v1 (𝜑𝐾𝑋)
lsppropd.v2 (𝜑𝐿𝑌)
Assertion
Ref Expression
lsspropdg (𝜑 → (LSubSp‘𝐾) = (LSubSp‘𝐿))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦   𝜑,𝑥,𝑦   𝑥,𝑊,𝑦   𝑥,𝐿,𝑦   𝑥,𝑃,𝑦
Allowed substitution hints:   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem lsspropdg
Dummy variables 𝑎 𝑏 𝑧 𝑠 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 527 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝜑)
2 simprl 529 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝑧𝑃)
3 simplr 528 . . . . . . . . . . . . . . 15 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝑠𝐵)
4 simprrl 539 . . . . . . . . . . . . . . 15 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝑎𝑠)
53, 4sseldd 3168 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝑎𝐵)
6 lsspropd.s1 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑃𝑦𝐵)) → (𝑥( ·𝑠𝐾)𝑦) ∈ 𝑊)
76ralrimivva 2569 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝑃𝑦𝐵 (𝑥( ·𝑠𝐾)𝑦) ∈ 𝑊)
87ad2antrr 488 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → ∀𝑥𝑃𝑦𝐵 (𝑥( ·𝑠𝐾)𝑦) ∈ 𝑊)
9 ovrspc2v 5914 . . . . . . . . . . . . . 14 (((𝑧𝑃𝑎𝐵) ∧ ∀𝑥𝑃𝑦𝐵 (𝑥( ·𝑠𝐾)𝑦) ∈ 𝑊) → (𝑧( ·𝑠𝐾)𝑎) ∈ 𝑊)
102, 5, 8, 9syl21anc 1247 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → (𝑧( ·𝑠𝐾)𝑎) ∈ 𝑊)
11 lsspropd.w . . . . . . . . . . . . . . 15 (𝜑𝐵𝑊)
1211ad2antrr 488 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝐵𝑊)
13 simprrr 540 . . . . . . . . . . . . . . 15 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝑏𝑠)
143, 13sseldd 3168 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝑏𝐵)
1512, 14sseldd 3168 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → 𝑏𝑊)
16 lsspropd.p . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑊𝑦𝑊)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
1716oveqrspc2v 5915 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑧( ·𝑠𝐾)𝑎) ∈ 𝑊𝑏𝑊)) → ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) = ((𝑧( ·𝑠𝐾)𝑎)(+g𝐿)𝑏))
181, 10, 15, 17syl12anc 1246 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) = ((𝑧( ·𝑠𝐾)𝑎)(+g𝐿)𝑏))
19 lsspropd.s2 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑃𝑦𝐵)) → (𝑥( ·𝑠𝐾)𝑦) = (𝑥( ·𝑠𝐿)𝑦))
2019oveqrspc2v 5915 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑃𝑎𝐵)) → (𝑧( ·𝑠𝐾)𝑎) = (𝑧( ·𝑠𝐿)𝑎))
211, 2, 5, 20syl12anc 1246 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → (𝑧( ·𝑠𝐾)𝑎) = (𝑧( ·𝑠𝐿)𝑎))
2221oveq1d 5903 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → ((𝑧( ·𝑠𝐾)𝑎)(+g𝐿)𝑏) = ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏))
2318, 22eqtrd 2220 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) = ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏))
2423eleq1d 2256 . . . . . . . . . 10 (((𝜑𝑠𝐵) ∧ (𝑧𝑃 ∧ (𝑎𝑠𝑏𝑠))) → (((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠 ↔ ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠))
2524anassrs 400 . . . . . . . . 9 ((((𝜑𝑠𝐵) ∧ 𝑧𝑃) ∧ (𝑎𝑠𝑏𝑠)) → (((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠 ↔ ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠))
26252ralbidva 2509 . . . . . . . 8 (((𝜑𝑠𝐵) ∧ 𝑧𝑃) → (∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠 ↔ ∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠))
2726ralbidva 2483 . . . . . . 7 ((𝜑𝑠𝐵) → (∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠 ↔ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠))
2827anbi2d 464 . . . . . 6 ((𝜑𝑠𝐵) → ((∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠) ↔ (∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠)))
2928pm5.32da 452 . . . . 5 (𝜑 → ((𝑠𝐵 ∧ (∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠)) ↔ (𝑠𝐵 ∧ (∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠))))
30 3anass 983 . . . . 5 ((𝑠𝐵 ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠) ↔ (𝑠𝐵 ∧ (∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠)))
31 3anass 983 . . . . 5 ((𝑠𝐵 ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠) ↔ (𝑠𝐵 ∧ (∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠)))
3229, 30, 313bitr4g 223 . . . 4 (𝜑 → ((𝑠𝐵 ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠) ↔ (𝑠𝐵 ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠)))
33 lsspropd.b1 . . . . . 6 (𝜑𝐵 = (Base‘𝐾))
3433sseq2d 3197 . . . . 5 (𝜑 → (𝑠𝐵𝑠 ⊆ (Base‘𝐾)))
35 lsspropd.p1 . . . . . 6 (𝜑𝑃 = (Base‘(Scalar‘𝐾)))
3635raleqdv 2689 . . . . 5 (𝜑 → (∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠 ↔ ∀𝑧 ∈ (Base‘(Scalar‘𝐾))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠))
3734, 363anbi13d 1324 . . . 4 (𝜑 → ((𝑠𝐵 ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ (Base‘𝐾) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐾))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠)))
38 lsspropd.b2 . . . . . 6 (𝜑𝐵 = (Base‘𝐿))
3938sseq2d 3197 . . . . 5 (𝜑 → (𝑠𝐵𝑠 ⊆ (Base‘𝐿)))
40 lsspropd.p2 . . . . . 6 (𝜑𝑃 = (Base‘(Scalar‘𝐿)))
4140raleqdv 2689 . . . . 5 (𝜑 → (∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠 ↔ ∀𝑧 ∈ (Base‘(Scalar‘𝐿))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠))
4239, 413anbi13d 1324 . . . 4 (𝜑 → ((𝑠𝐵 ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧𝑃𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ (Base‘𝐿) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐿))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠)))
4332, 37, 423bitr3d 218 . . 3 (𝜑 → ((𝑠 ⊆ (Base‘𝐾) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐾))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ (Base‘𝐿) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐿))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠)))
44 lsppropd.v1 . . . 4 (𝜑𝐾𝑋)
45 eqid 2187 . . . . 5 (Scalar‘𝐾) = (Scalar‘𝐾)
46 eqid 2187 . . . . 5 (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐾))
47 eqid 2187 . . . . 5 (Base‘𝐾) = (Base‘𝐾)
48 eqid 2187 . . . . 5 (+g𝐾) = (+g𝐾)
49 eqid 2187 . . . . 5 ( ·𝑠𝐾) = ( ·𝑠𝐾)
50 eqid 2187 . . . . 5 (LSubSp‘𝐾) = (LSubSp‘𝐾)
5145, 46, 47, 48, 49, 50islssmg 13542 . . . 4 (𝐾𝑋 → (𝑠 ∈ (LSubSp‘𝐾) ↔ (𝑠 ⊆ (Base‘𝐾) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐾))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠)))
5244, 51syl 14 . . 3 (𝜑 → (𝑠 ∈ (LSubSp‘𝐾) ↔ (𝑠 ⊆ (Base‘𝐾) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐾))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐾)𝑎)(+g𝐾)𝑏) ∈ 𝑠)))
53 lsppropd.v2 . . . 4 (𝜑𝐿𝑌)
54 eqid 2187 . . . . 5 (Scalar‘𝐿) = (Scalar‘𝐿)
55 eqid 2187 . . . . 5 (Base‘(Scalar‘𝐿)) = (Base‘(Scalar‘𝐿))
56 eqid 2187 . . . . 5 (Base‘𝐿) = (Base‘𝐿)
57 eqid 2187 . . . . 5 (+g𝐿) = (+g𝐿)
58 eqid 2187 . . . . 5 ( ·𝑠𝐿) = ( ·𝑠𝐿)
59 eqid 2187 . . . . 5 (LSubSp‘𝐿) = (LSubSp‘𝐿)
6054, 55, 56, 57, 58, 59islssmg 13542 . . . 4 (𝐿𝑌 → (𝑠 ∈ (LSubSp‘𝐿) ↔ (𝑠 ⊆ (Base‘𝐿) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐿))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠)))
6153, 60syl 14 . . 3 (𝜑 → (𝑠 ∈ (LSubSp‘𝐿) ↔ (𝑠 ⊆ (Base‘𝐿) ∧ ∃𝑗 𝑗𝑠 ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝐿))∀𝑎𝑠𝑏𝑠 ((𝑧( ·𝑠𝐿)𝑎)(+g𝐿)𝑏) ∈ 𝑠)))
6243, 52, 613bitr4d 220 . 2 (𝜑 → (𝑠 ∈ (LSubSp‘𝐾) ↔ 𝑠 ∈ (LSubSp‘𝐿)))
6362eqrdv 2185 1 (𝜑 → (LSubSp‘𝐾) = (LSubSp‘𝐿))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 979   = wceq 1363  wex 1502  wcel 2158  wral 2465  wss 3141  cfv 5228  (class class class)co 5888  Basecbs 12475  +gcplusg 12550  Scalarcsca 12553   ·𝑠 cvsca 12554  LSubSpclss 13536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-cnex 7915  ax-resscn 7916  ax-1re 7918  ax-addrcl 7921
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-iota 5190  df-fun 5230  df-fn 5231  df-fv 5236  df-ov 5891  df-inn 8933  df-ndx 12478  df-slot 12479  df-base 12481  df-lssm 13537
This theorem is referenced by:  lsppropd  13616
  Copyright terms: Public domain W3C validator