Metamath Proof Explorer

Theorem cdj3lem2

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

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

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 
 |-  A e. SH
2 cdj3lem2.2 
 |-  B e. SH
3 cdj3lem2.3 
 |-  S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )
4 1 2 shsvai 
 |-  ( ( C e. A /\ D e. B ) -> ( C +h D ) e. ( A +H B ) )
5 eqeq1 
 |-  ( x = ( C +h D ) -> ( x = ( z +h w ) <-> ( C +h D ) = ( z +h w ) ) )
6 5 rexbidv 
 |-  ( x = ( C +h D ) -> ( E. w e. B x = ( z +h w ) <-> E. w e. B ( C +h D ) = ( z +h w ) ) )
7 6 riotabidv 
 |-  ( x = ( C +h D ) -> ( iota_ z e. A E. w e. B x = ( z +h w ) ) = ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) )
8 riotaex 
 |-  ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) e. _V
9 7 3 8 fvmpt 
 |-  ( ( C +h D ) e. ( A +H B ) -> ( S ` ( C +h D ) ) = ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) )
10 4 9 syl 
 |-  ( ( C e. A /\ D e. B ) -> ( S ` ( C +h D ) ) = ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) )
11 10 3adant3 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( S ` ( C +h D ) ) = ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) )
12 eqid 
 |-  ( C +h D ) = ( C +h D )
13 oveq2 
 |-  ( w = D -> ( C +h w ) = ( C +h D ) )
14 13 rspceeqv 
 |-  ( ( D e. B /\ ( C +h D ) = ( C +h D ) ) -> E. w e. B ( C +h D ) = ( C +h w ) )
15 12 14 mpan2 
 |-  ( D e. B -> E. w e. B ( C +h D ) = ( C +h w ) )
16 15 3ad2ant2 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> E. w e. B ( C +h D ) = ( C +h w ) )
17 simp1 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> C e. A )
18 1 2 cdjreui 
 |-  ( ( ( C +h D ) e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> E! z e. A E. w e. B ( C +h D ) = ( z +h w ) )
19 4 18 stoic3 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> E! z e. A E. w e. B ( C +h D ) = ( z +h w ) )
20 oveq1 
 |-  ( z = C -> ( z +h w ) = ( C +h w ) )
21 20 eqeq2d 
 |-  ( z = C -> ( ( C +h D ) = ( z +h w ) <-> ( C +h D ) = ( C +h w ) ) )
22 21 rexbidv 
 |-  ( z = C -> ( E. w e. B ( C +h D ) = ( z +h w ) <-> E. w e. B ( C +h D ) = ( C +h w ) ) )
23 22 riota2 
 |-  ( ( C e. A /\ E! z e. A E. w e. B ( C +h D ) = ( z +h w ) ) -> ( E. w e. B ( C +h D ) = ( C +h w ) <-> ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) = C ) )
24 17 19 23 syl2anc 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( E. w e. B ( C +h D ) = ( C +h w ) <-> ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) = C ) )
25 16 24 mpbid 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( iota_ z e. A E. w e. B ( C +h D ) = ( z +h w ) ) = C )
26 11 25 eqtrd 
 |-  ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( S ` ( C +h D ) ) = C )