Step |
Hyp |
Ref |
Expression |
1 |
|
ltrnj.b |
|- B = ( Base ` K ) |
2 |
|
ltrnj.j |
|- .\/ = ( join ` K ) |
3 |
|
ltrnj.h |
|- H = ( LHyp ` K ) |
4 |
|
ltrnj.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> K e. HL ) |
6 |
5
|
hllatd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> K e. Lat ) |
7 |
|
eqid |
|- ( LAut ` K ) = ( LAut ` K ) |
8 |
3 7 4
|
ltrnlaut |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( LAut ` K ) ) |
9 |
8
|
3adant3 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> F e. ( LAut ` K ) ) |
10 |
|
simp3l |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> X e. B ) |
11 |
|
simp3r |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> Y e. B ) |
12 |
1 2 7
|
lautj |
|- ( ( K e. Lat /\ ( F e. ( LAut ` K ) /\ X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) ) |
13 |
6 9 10 11 12
|
syl13anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) ) |