Metamath Proof Explorer

Theorem cdj3lem3

Description: Lemma for cdj3i . Value of the second-component function T . (Contributed by NM, 23-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj3lem2.1 
|- A e. SH
cdj3lem2.2 
|- B e. SH
cdj3lem3.3 
|- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
Assertion cdj3lem3 
|- ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( T ` ( C +h D ) ) = D )

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 
 |-  A e. SH
2 cdj3lem2.2 
 |-  B e. SH
3 cdj3lem3.3 
 |-  T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
4 incom 
 |-  ( A i^i B ) = ( B i^i A )
5 4 eqeq1i 
 |-  ( ( A i^i B ) = 0H <-> ( B i^i A ) = 0H )
6 2 sheli 
 |-  ( D e. B -> D e. ~H )
7 1 sheli 
 |-  ( C e. A -> C e. ~H )
8 ax-hvcom 
 |-  ( ( D e. ~H /\ C e. ~H ) -> ( D +h C ) = ( C +h D ) )
9 6 7 8 syl2an 
 |-  ( ( D e. B /\ C e. A ) -> ( D +h C ) = ( C +h D ) )
10 9 fveq2d 
 |-  ( ( D e. B /\ C e. A ) -> ( T ` ( D +h C ) ) = ( T ` ( C +h D ) ) )
11 10 3adant3 
 |-  ( ( D e. B /\ C e. A /\ ( B i^i A ) = 0H ) -> ( T ` ( D +h C ) ) = ( T ` ( C +h D ) ) )
12 2 1 shscomi 
 |-  ( B +H A ) = ( A +H B )
13 2 sheli 
 |-  ( w e. B -> w e. ~H )
14 1 sheli 
 |-  ( z e. A -> z e. ~H )
15 ax-hvcom 
 |-  ( ( w e. ~H /\ z e. ~H ) -> ( w +h z ) = ( z +h w ) )
16 13 14 15 syl2an 
 |-  ( ( w e. B /\ z e. A ) -> ( w +h z ) = ( z +h w ) )
17 16 eqeq2d 
 |-  ( ( w e. B /\ z e. A ) -> ( x = ( w +h z ) <-> x = ( z +h w ) ) )
18 17 rexbidva 
 |-  ( w e. B -> ( E. z e. A x = ( w +h z ) <-> E. z e. A x = ( z +h w ) ) )
19 18 riotabiia 
 |-  ( iota_ w e. B E. z e. A x = ( w +h z ) ) = ( iota_ w e. B E. z e. A x = ( z +h w ) )
20 12 19 mpteq12i 
 |-  ( x e. ( B +H A ) |-> ( iota_ w e. B E. z e. A x = ( w +h z ) ) ) = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
21 3 20 eqtr4i 
 |-  T = ( x e. ( B +H A ) |-> ( iota_ w e. B E. z e. A x = ( w +h z ) ) )
22 2 1 21 cdj3lem2 
 |-  ( ( D e. B /\ C e. A /\ ( B i^i A ) = 0H ) -> ( T ` ( D +h C ) ) = D )
23 11 22 eqtr3d 
 |-  ( ( D e. B /\ C e. A /\ ( B i^i A ) = 0H ) -> ( T ` ( C +h D ) ) = D )
24 5 23 syl3an3b 
 |-  ( ( D e. B /\ C e. A /\ ( A i^i B ) = 0H ) -> ( T ` ( C +h D ) ) = D )
25 24 3com12 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( T ` ( C +h D ) ) = D )