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

Theorem lsspropdg 13584
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 13511 . . . 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 13511 . . . 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 13505
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 13506
This theorem is referenced by:  lsppropd  13585
  Copyright terms: Public domain W3C validator