# 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}\in {\mathbf{S}}_{ℋ}$
cdj3lem2.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
cdj3lem2.3 ${⊢}{S}=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)\right)$
Assertion cdj3lem2 ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({C}{+}_{ℎ}{D}\right)={C}$

### Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
2 cdj3lem2.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
3 cdj3lem2.3 ${⊢}{S}=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)\right)$
4 1 2 shsvai ${⊢}\left({C}\in {A}\wedge {D}\in {B}\right)\to {C}{+}_{ℎ}{D}\in \left({A}{+}_{ℋ}{B}\right)$
5 eqeq1 ${⊢}{x}={C}{+}_{ℎ}{D}\to \left({x}={z}{+}_{ℎ}{w}↔{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)$
6 5 rexbidv ${⊢}{x}={C}{+}_{ℎ}{D}\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)$
7 6 riotabidv ${⊢}{x}={C}{+}_{ℎ}{D}\to \left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)=\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)$
8 riotaex ${⊢}\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)\in \mathrm{V}$
9 7 3 8 fvmpt ${⊢}{C}{+}_{ℎ}{D}\in \left({A}{+}_{ℋ}{B}\right)\to {S}\left({C}{+}_{ℎ}{D}\right)=\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)$
10 4 9 syl ${⊢}\left({C}\in {A}\wedge {D}\in {B}\right)\to {S}\left({C}{+}_{ℎ}{D}\right)=\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)$
11 10 3adant3 ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({C}{+}_{ℎ}{D}\right)=\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)$
12 eqid ${⊢}{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{D}$
13 oveq2 ${⊢}{w}={D}\to {C}{+}_{ℎ}{w}={C}{+}_{ℎ}{D}$
14 13 rspceeqv ${⊢}\left({D}\in {B}\wedge {C}{+}_{ℎ}{D}={C}{+}_{ℎ}{D}\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{w}$
15 12 14 mpan2 ${⊢}{D}\in {B}\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{w}$
16 15 3ad2ant2 ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{w}$
17 simp1 ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {C}\in {A}$
18 1 2 cdjreui ${⊢}\left({C}{+}_{ℎ}{D}\in \left({A}{+}_{ℋ}{B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to \exists !{z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}$
19 4 18 stoic3 ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to \exists !{z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}$
20 oveq1 ${⊢}{z}={C}\to {z}{+}_{ℎ}{w}={C}{+}_{ℎ}{w}$
21 20 eqeq2d ${⊢}{z}={C}\to \left({C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}↔{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{w}\right)$
22 21 rexbidv ${⊢}{z}={C}\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{w}\right)$
23 22 riota2 ${⊢}\left({C}\in {A}\wedge \exists !{z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{w}↔\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)={C}\right)$
24 17 19 23 syl2anc ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={C}{+}_{ℎ}{w}↔\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)={C}\right)$
25 16 24 mpbid ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to \left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{+}_{ℎ}{D}={z}{+}_{ℎ}{w}\right)={C}$
26 11 25 eqtrd ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({C}{+}_{ℎ}{D}\right)={C}$