Metamath Proof Explorer


Theorem lbspropd

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

Ref Expression
Hypotheses lbspropd.b1 โŠข ( ๐œ‘ โ†’ ๐ต = ( Base โ€˜ ๐พ ) )
lbspropd.b2 โŠข ( ๐œ‘ โ†’ ๐ต = ( Base โ€˜ ๐ฟ ) )
lbspropd.w โŠข ( ๐œ‘ โ†’ ๐ต โŠ† ๐‘Š )
lbspropd.p โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘Š โˆง ๐‘ฆ โˆˆ ๐‘Š ) ) โ†’ ( ๐‘ฅ ( +g โ€˜ ๐พ ) ๐‘ฆ ) = ( ๐‘ฅ ( +g โ€˜ ๐ฟ ) ๐‘ฆ ) )
lbspropd.s1 โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐ต ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ฆ ) โˆˆ ๐‘Š )
lbspropd.s2 โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐ต ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ฆ ) = ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ฆ ) )
lbspropd.f โŠข ๐น = ( Scalar โ€˜ ๐พ )
lbspropd.g โŠข ๐บ = ( Scalar โ€˜ ๐ฟ )
lbspropd.p1 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐น ) )
lbspropd.p2 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐บ ) )
lbspropd.a โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘ƒ ) ) โ†’ ( ๐‘ฅ ( +g โ€˜ ๐น ) ๐‘ฆ ) = ( ๐‘ฅ ( +g โ€˜ ๐บ ) ๐‘ฆ ) )
lbspropd.v1 โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ๐‘‹ )
lbspropd.v2 โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ๐‘Œ )
Assertion lbspropd ( ๐œ‘ โ†’ ( LBasis โ€˜ ๐พ ) = ( LBasis โ€˜ ๐ฟ ) )

Proof

Step Hyp Ref Expression
1 lbspropd.b1 โŠข ( ๐œ‘ โ†’ ๐ต = ( Base โ€˜ ๐พ ) )
2 lbspropd.b2 โŠข ( ๐œ‘ โ†’ ๐ต = ( Base โ€˜ ๐ฟ ) )
3 lbspropd.w โŠข ( ๐œ‘ โ†’ ๐ต โŠ† ๐‘Š )
4 lbspropd.p โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘Š โˆง ๐‘ฆ โˆˆ ๐‘Š ) ) โ†’ ( ๐‘ฅ ( +g โ€˜ ๐พ ) ๐‘ฆ ) = ( ๐‘ฅ ( +g โ€˜ ๐ฟ ) ๐‘ฆ ) )
5 lbspropd.s1 โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐ต ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ฆ ) โˆˆ ๐‘Š )
6 lbspropd.s2 โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐ต ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ฆ ) = ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ฆ ) )
7 lbspropd.f โŠข ๐น = ( Scalar โ€˜ ๐พ )
8 lbspropd.g โŠข ๐บ = ( Scalar โ€˜ ๐ฟ )
9 lbspropd.p1 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐น ) )
10 lbspropd.p2 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐บ ) )
11 lbspropd.a โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘ƒ ) ) โ†’ ( ๐‘ฅ ( +g โ€˜ ๐น ) ๐‘ฆ ) = ( ๐‘ฅ ( +g โ€˜ ๐บ ) ๐‘ฆ ) )
12 lbspropd.v1 โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ๐‘‹ )
13 lbspropd.v2 โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ๐‘Œ )
14 simplll โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ๐œ‘ )
15 eldifi โŠข ( ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) โ†’ ๐‘ฃ โˆˆ ๐‘ƒ )
16 15 adantl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ๐‘ฃ โˆˆ ๐‘ƒ )
17 simpr โŠข ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โ†’ ๐‘ง โŠ† ๐ต )
18 17 sselda โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ๐‘ข โˆˆ ๐ต )
19 18 adantr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ๐‘ข โˆˆ ๐ต )
20 6 oveqrspc2v โŠข ( ( ๐œ‘ โˆง ( ๐‘ฃ โˆˆ ๐‘ƒ โˆง ๐‘ข โˆˆ ๐ต ) ) โ†’ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) = ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) )
21 14 16 19 20 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) = ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) )
22 7 fveq2i โŠข ( Base โ€˜ ๐น ) = ( Base โ€˜ ( Scalar โ€˜ ๐พ ) )
23 9 22 eqtrdi โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ( Scalar โ€˜ ๐พ ) ) )
24 8 fveq2i โŠข ( Base โ€˜ ๐บ ) = ( Base โ€˜ ( Scalar โ€˜ ๐ฟ ) )
25 10 24 eqtrdi โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ( Scalar โ€˜ ๐ฟ ) ) )
26 1 2 3 4 5 6 23 25 12 13 lsppropd โŠข ( ๐œ‘ โ†’ ( LSpan โ€˜ ๐พ ) = ( LSpan โ€˜ ๐ฟ ) )
27 14 26 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ( LSpan โ€˜ ๐พ ) = ( LSpan โ€˜ ๐ฟ ) )
28 27 fveq1d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) = ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) )
29 21 28 eleq12d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ( ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) โ†” ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) )
30 29 notbid โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โˆง ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ) โ†’ ( ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) โ†” ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) )
31 30 ralbidva โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ( โˆ€ ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) โ†” โˆ€ ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) )
32 9 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ๐‘ƒ = ( Base โ€˜ ๐น ) )
33 32 difeq1d โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) = ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) )
34 33 raleqdv โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ( โˆ€ ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) โ†” โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) )
35 10 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ๐‘ƒ = ( Base โ€˜ ๐บ ) )
36 9 10 11 grpidpropd โŠข ( ๐œ‘ โ†’ ( 0g โ€˜ ๐น ) = ( 0g โ€˜ ๐บ ) )
37 36 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ( 0g โ€˜ ๐น ) = ( 0g โ€˜ ๐บ ) )
38 37 sneqd โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ { ( 0g โ€˜ ๐น ) } = { ( 0g โ€˜ ๐บ ) } )
39 35 38 difeq12d โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) = ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) )
40 39 raleqdv โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ( โˆ€ ๐‘ฃ โˆˆ ( ๐‘ƒ โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) โ†” โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) )
41 31 34 40 3bitr3d โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โˆง ๐‘ข โˆˆ ๐‘ง ) โ†’ ( โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) โ†” โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) )
42 41 ralbidva โŠข ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โ†’ ( โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) โ†” โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) )
43 42 anbi2d โŠข ( ( ๐œ‘ โˆง ๐‘ง โŠ† ๐ต ) โ†’ ( ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) โ†” ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
44 43 pm5.32da โŠข ( ๐œ‘ โ†’ ( ( ๐‘ง โŠ† ๐ต โˆง ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) โ†” ( ๐‘ง โŠ† ๐ต โˆง ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) ) )
45 1 sseq2d โŠข ( ๐œ‘ โ†’ ( ๐‘ง โŠ† ๐ต โ†” ๐‘ง โŠ† ( Base โ€˜ ๐พ ) ) )
46 45 anbi1d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ง โŠ† ๐ต โˆง ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐พ ) โˆง ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) ) )
47 2 sseq2d โŠข ( ๐œ‘ โ†’ ( ๐‘ง โŠ† ๐ต โ†” ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) ) )
48 26 fveq1d โŠข ( ๐œ‘ โ†’ ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) )
49 1 2 eqtr3d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐พ ) = ( Base โ€˜ ๐ฟ ) )
50 48 49 eqeq12d โŠข ( ๐œ‘ โ†’ ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โ†” ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) ) )
51 50 anbi1d โŠข ( ๐œ‘ โ†’ ( ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) โ†” ( ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
52 47 51 anbi12d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ง โŠ† ๐ต โˆง ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) โˆง ( ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) ) )
53 44 46 52 3bitr3d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ง โŠ† ( Base โ€˜ ๐พ ) โˆง ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) โˆง ( ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) ) )
54 3anass โŠข ( ( ๐‘ง โŠ† ( Base โ€˜ ๐พ ) โˆง ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐พ ) โˆง ( ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
55 3anass โŠข ( ( ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) โˆง ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) โˆง ( ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
56 53 54 55 3bitr4g โŠข ( ๐œ‘ โ†’ ( ( ๐‘ง โŠ† ( Base โ€˜ ๐พ ) โˆง ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) โˆง ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
57 eqid โŠข ( Base โ€˜ ๐พ ) = ( Base โ€˜ ๐พ )
58 eqid โŠข ( ยท๐‘  โ€˜ ๐พ ) = ( ยท๐‘  โ€˜ ๐พ )
59 eqid โŠข ( Base โ€˜ ๐น ) = ( Base โ€˜ ๐น )
60 eqid โŠข ( LBasis โ€˜ ๐พ ) = ( LBasis โ€˜ ๐พ )
61 eqid โŠข ( LSpan โ€˜ ๐พ ) = ( LSpan โ€˜ ๐พ )
62 eqid โŠข ( 0g โ€˜ ๐น ) = ( 0g โ€˜ ๐น )
63 57 7 58 59 60 61 62 islbs โŠข ( ๐พ โˆˆ ๐‘‹ โ†’ ( ๐‘ง โˆˆ ( LBasis โ€˜ ๐พ ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐พ ) โˆง ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
64 12 63 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ง โˆˆ ( LBasis โ€˜ ๐พ ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐พ ) โˆง ( ( LSpan โ€˜ ๐พ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐พ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐น ) โˆ– { ( 0g โ€˜ ๐น ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐พ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
65 eqid โŠข ( Base โ€˜ ๐ฟ ) = ( Base โ€˜ ๐ฟ )
66 eqid โŠข ( ยท๐‘  โ€˜ ๐ฟ ) = ( ยท๐‘  โ€˜ ๐ฟ )
67 eqid โŠข ( Base โ€˜ ๐บ ) = ( Base โ€˜ ๐บ )
68 eqid โŠข ( LBasis โ€˜ ๐ฟ ) = ( LBasis โ€˜ ๐ฟ )
69 eqid โŠข ( LSpan โ€˜ ๐ฟ ) = ( LSpan โ€˜ ๐ฟ )
70 eqid โŠข ( 0g โ€˜ ๐บ ) = ( 0g โ€˜ ๐บ )
71 65 8 66 67 68 69 70 islbs โŠข ( ๐ฟ โˆˆ ๐‘Œ โ†’ ( ๐‘ง โˆˆ ( LBasis โ€˜ ๐ฟ ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) โˆง ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
72 13 71 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ง โˆˆ ( LBasis โ€˜ ๐ฟ ) โ†” ( ๐‘ง โŠ† ( Base โ€˜ ๐ฟ ) โˆง ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ๐‘ง ) = ( Base โ€˜ ๐ฟ ) โˆง โˆ€ ๐‘ข โˆˆ ๐‘ง โˆ€ ๐‘ฃ โˆˆ ( ( Base โ€˜ ๐บ ) โˆ– { ( 0g โ€˜ ๐บ ) } ) ยฌ ( ๐‘ฃ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ข ) โˆˆ ( ( LSpan โ€˜ ๐ฟ ) โ€˜ ( ๐‘ง โˆ– { ๐‘ข } ) ) ) ) )
73 56 64 72 3bitr4d โŠข ( ๐œ‘ โ†’ ( ๐‘ง โˆˆ ( LBasis โ€˜ ๐พ ) โ†” ๐‘ง โˆˆ ( LBasis โ€˜ ๐ฟ ) ) )
74 73 eqrdv โŠข ( ๐œ‘ โ†’ ( LBasis โ€˜ ๐พ ) = ( LBasis โ€˜ ๐ฟ ) )