Step |
Hyp |
Ref |
Expression |
1 |
|
lsmless2.v |
|- B = ( Base ` G ) |
2 |
|
lsmless2.s |
|- .(+) = ( LSSum ` G ) |
3 |
|
ssrexv |
|- ( R C_ T -> ( E. y e. R E. z e. U x = ( y ( +g ` G ) z ) -> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) ) |
4 |
3
|
adantl |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( E. y e. R E. z e. U x = ( y ( +g ` G ) z ) -> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) ) |
5 |
|
simpl1 |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> G e. V ) |
6 |
|
simpr |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> R C_ T ) |
7 |
|
simpl2 |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> T C_ B ) |
8 |
6 7
|
sstrd |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> R C_ B ) |
9 |
|
simpl3 |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> U C_ B ) |
10 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
11 |
1 10 2
|
lsmelvalx |
|- ( ( G e. V /\ R C_ B /\ U C_ B ) -> ( x e. ( R .(+) U ) <-> E. y e. R E. z e. U x = ( y ( +g ` G ) z ) ) ) |
12 |
5 8 9 11
|
syl3anc |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( x e. ( R .(+) U ) <-> E. y e. R E. z e. U x = ( y ( +g ` G ) z ) ) ) |
13 |
1 10 2
|
lsmelvalx |
|- ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( x e. ( T .(+) U ) <-> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) ) |
14 |
13
|
adantr |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( x e. ( T .(+) U ) <-> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) ) |
15 |
4 12 14
|
3imtr4d |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( x e. ( R .(+) U ) -> x e. ( T .(+) U ) ) ) |
16 |
15
|
ssrdv |
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( R .(+) U ) C_ ( T .(+) U ) ) |