Metamath Proof Explorer

Theorem dihjat2

Description: The subspace sum of a closed subspace and an atom is the same as their subspace join. (Contributed by NM, 1-Oct-2014)

Ref Expression
Hypotheses dihjat2.h 
|- H = ( LHyp ` K )
dihjat2.i 
|- I = ( ( DIsoH ` K ) ` W )
dihjat2.j 
|- .\/ = ( ( joinH ` K ) ` W )
dihjat2.u 
|- U = ( ( DVecH ` K ) ` W )
dihjat2.p 
|- .(+) = ( LSSum ` U )
dihjat2.a 
|- A = ( LSAtoms ` U )
dihjat2.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihjat2.x 
|- ( ph -> X e. ran I )
dihjat2.q 
|- ( ph -> Q e. A )
Assertion dihjat2 
|- ( ph -> ( X .\/ Q ) = ( X .(+) Q ) )

Proof

Step Hyp Ref Expression
1 dihjat2.h 
 |-  H = ( LHyp ` K )
2 dihjat2.i 
 |-  I = ( ( DIsoH ` K ) ` W )
3 dihjat2.j 
 |-  .\/ = ( ( joinH ` K ) ` W )
4 dihjat2.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihjat2.p 
 |-  .(+) = ( LSSum ` U )
6 dihjat2.a 
 |-  A = ( LSAtoms ` U )
7 dihjat2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 dihjat2.x 
 |-  ( ph -> X e. ran I )
9 dihjat2.q 
 |-  ( ph -> Q e. A )
10 eqid 
 |-  ( Base ` U ) = ( Base ` U )
11 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
12 7 adantr 
 |-  ( ( ph /\ v e. ( Base ` U ) ) -> ( K e. HL /\ W e. H ) )
13 8 adantr 
 |-  ( ( ph /\ v e. ( Base ` U ) ) -> X e. ran I )
14 simpr 
 |-  ( ( ph /\ v e. ( Base ` U ) ) -> v e. ( Base ` U ) )
15 1 4 10 5 11 2 3 12 13 14 dihjat1 
 |-  ( ( ph /\ v e. ( Base ` U ) ) -> ( X .\/ ( ( LSpan ` U ) ` { v } ) ) = ( X .(+) ( ( LSpan ` U ) ` { v } ) ) )
16 15 adantr 
 |-  ( ( ( ph /\ v e. ( Base ` U ) ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> ( X .\/ ( ( LSpan ` U ) ` { v } ) ) = ( X .(+) ( ( LSpan ` U ) ` { v } ) ) )
17 oveq2 
 |-  ( Q = ( ( LSpan ` U ) ` { v } ) -> ( X .\/ Q ) = ( X .\/ ( ( LSpan ` U ) ` { v } ) ) )
18 17 adantl 
 |-  ( ( ( ph /\ v e. ( Base ` U ) ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> ( X .\/ Q ) = ( X .\/ ( ( LSpan ` U ) ` { v } ) ) )
19 oveq2 
 |-  ( Q = ( ( LSpan ` U ) ` { v } ) -> ( X .(+) Q ) = ( X .(+) ( ( LSpan ` U ) ` { v } ) ) )
20 19 adantl 
 |-  ( ( ( ph /\ v e. ( Base ` U ) ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> ( X .(+) Q ) = ( X .(+) ( ( LSpan ` U ) ` { v } ) ) )
21 16 18 20 3eqtr4d 
 |-  ( ( ( ph /\ v e. ( Base ` U ) ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> ( X .\/ Q ) = ( X .(+) Q ) )
22 1 4 7 dvhlmod 
 |-  ( ph -> U e. LMod )
23 10 11 6 islsati 
 |-  ( ( U e. LMod /\ Q e. A ) -> E. v e. ( Base ` U ) Q = ( ( LSpan ` U ) ` { v } ) )
24 22 9 23 syl2anc 
 |-  ( ph -> E. v e. ( Base ` U ) Q = ( ( LSpan ` U ) ` { v } ) )
25 21 24 r19.29a 
 |-  ( ph -> ( X .\/ Q ) = ( X .(+) Q ) )