Metamath Proof Explorer


Theorem lsppropd

Description: If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015) (Revised by AV, 24-Apr-2024)

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 โ€˜ ๐ฟ ) ) )
lsppropd.v1 โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ๐‘‹ )
lsppropd.v2 โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ๐‘Œ )
Assertion lsppropd ( ๐œ‘ โ†’ ( LSpan โ€˜ ๐พ ) = ( LSpan โ€˜ ๐ฟ ) )

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 lsppropd.v1 โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ๐‘‹ )
10 lsppropd.v2 โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ๐‘Œ )
11 1 2 eqtr3d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐พ ) = ( Base โ€˜ ๐ฟ ) )
12 11 pweqd โŠข ( ๐œ‘ โ†’ ๐’ซ ( Base โ€˜ ๐พ ) = ๐’ซ ( Base โ€˜ ๐ฟ ) )
13 1 2 3 4 5 6 7 8 lsspropd โŠข ( ๐œ‘ โ†’ ( LSubSp โ€˜ ๐พ ) = ( LSubSp โ€˜ ๐ฟ ) )
14 13 rabeqdv โŠข ( ๐œ‘ โ†’ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐พ ) โˆฃ ๐‘  โŠ† ๐‘ก } = { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐ฟ ) โˆฃ ๐‘  โŠ† ๐‘ก } )
15 14 inteqd โŠข ( ๐œ‘ โ†’ โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐พ ) โˆฃ ๐‘  โŠ† ๐‘ก } = โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐ฟ ) โˆฃ ๐‘  โŠ† ๐‘ก } )
16 12 15 mpteq12dv โŠข ( ๐œ‘ โ†’ ( ๐‘  โˆˆ ๐’ซ ( Base โ€˜ ๐พ ) โ†ฆ โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐พ ) โˆฃ ๐‘  โŠ† ๐‘ก } ) = ( ๐‘  โˆˆ ๐’ซ ( Base โ€˜ ๐ฟ ) โ†ฆ โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐ฟ ) โˆฃ ๐‘  โŠ† ๐‘ก } ) )
17 eqid โŠข ( Base โ€˜ ๐พ ) = ( Base โ€˜ ๐พ )
18 eqid โŠข ( LSubSp โ€˜ ๐พ ) = ( LSubSp โ€˜ ๐พ )
19 eqid โŠข ( LSpan โ€˜ ๐พ ) = ( LSpan โ€˜ ๐พ )
20 17 18 19 lspfval โŠข ( ๐พ โˆˆ ๐‘‹ โ†’ ( LSpan โ€˜ ๐พ ) = ( ๐‘  โˆˆ ๐’ซ ( Base โ€˜ ๐พ ) โ†ฆ โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐พ ) โˆฃ ๐‘  โŠ† ๐‘ก } ) )
21 9 20 syl โŠข ( ๐œ‘ โ†’ ( LSpan โ€˜ ๐พ ) = ( ๐‘  โˆˆ ๐’ซ ( Base โ€˜ ๐พ ) โ†ฆ โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐พ ) โˆฃ ๐‘  โŠ† ๐‘ก } ) )
22 eqid โŠข ( Base โ€˜ ๐ฟ ) = ( Base โ€˜ ๐ฟ )
23 eqid โŠข ( LSubSp โ€˜ ๐ฟ ) = ( LSubSp โ€˜ ๐ฟ )
24 eqid โŠข ( LSpan โ€˜ ๐ฟ ) = ( LSpan โ€˜ ๐ฟ )
25 22 23 24 lspfval โŠข ( ๐ฟ โˆˆ ๐‘Œ โ†’ ( LSpan โ€˜ ๐ฟ ) = ( ๐‘  โˆˆ ๐’ซ ( Base โ€˜ ๐ฟ ) โ†ฆ โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐ฟ ) โˆฃ ๐‘  โŠ† ๐‘ก } ) )
26 10 25 syl โŠข ( ๐œ‘ โ†’ ( LSpan โ€˜ ๐ฟ ) = ( ๐‘  โˆˆ ๐’ซ ( Base โ€˜ ๐ฟ ) โ†ฆ โˆฉ { ๐‘ก โˆˆ ( LSubSp โ€˜ ๐ฟ ) โˆฃ ๐‘  โŠ† ๐‘ก } ) )
27 16 21 26 3eqtr4d โŠข ( ๐œ‘ โ†’ ( LSpan โ€˜ ๐พ ) = ( LSpan โ€˜ ๐ฟ ) )