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

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		cdj3lem2.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		cdj3lem2.3	$$⊢S=\left(x\in \left(A{+}_{\mathscr{H}}B\right)⟼\left(\iota z\in A|\exists w\in Bx=z{+}_{ℎ}w\right)\right)$$
4	1 2	shsvai	$$⊢\left(C\in A\wedge D\in B\right)\to C{+}_{ℎ}D\in \left(A{+}_{\mathscr{H}}B\right)$$
5		eqeq1	$$⊢x=C{+}_{ℎ}D\to \left(x=z{+}_{ℎ}w\leftrightarrow C{+}_{ℎ}D=z{+}_{ℎ}w\right)$$
6	5	rexbidv	$$⊢x=C{+}_{ℎ}D\to \left(\exists w\in Bx=z{+}_{ℎ}w\leftrightarrow \exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\right)$$
7	6	riotabidv	$$⊢x=C{+}_{ℎ}D\to \left(\iota z\in A|\exists w\in Bx=z{+}_{ℎ}w\right)=\left(\iota z\in A|\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\right)$$
8		riotaex	$$⊢\left(\iota z\in A|\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\right)\in \mathrm{V}$$
9	7 3 8	fvmpt	$$⊢C{+}_{ℎ}D\in \left(A{+}_{\mathscr{H}}B\right)\to S\left(C{+}_{ℎ}D\right)=\left(\iota z\in A|\exists w\in BC{+}_{ℎ}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 BC{+}_{ℎ}D=z{+}_{ℎ}w\right)$$
11	10	3adant3	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to S\left(C{+}_{ℎ}D\right)=\left(\iota z\in A|\exists w\in BC{+}_{ℎ}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 BC{+}_{ℎ}D=C{+}_{ℎ}w$$
15	12 14	mpan2	$$⊢D\in B\to \exists w\in BC{+}_{ℎ}D=C{+}_{ℎ}w$$
16	15	3ad2ant2	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to \exists w\in BC{+}_{ℎ}D=C{+}_{ℎ}w$$
17		simp1	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to C\in A$$
18	1 2	cdjreui	$$⊢\left(C{+}_{ℎ}D\in \left(A{+}_{\mathscr{H}}B\right)\wedge A\cap B=0_{\mathscr{H}}\right)\to \exists !z\in A\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w$$
19	4 18	stoic3	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to \exists !z\in A\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w$$
20		oveq1	$$⊢z=C\to z{+}_{ℎ}w=C{+}_{ℎ}w$$
21	20	eqeq2d	$$⊢z=C\to \left(C{+}_{ℎ}D=z{+}_{ℎ}w\leftrightarrow C{+}_{ℎ}D=C{+}_{ℎ}w\right)$$
22	21	rexbidv	$$⊢z=C\to \left(\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\leftrightarrow \exists w\in BC{+}_{ℎ}D=C{+}_{ℎ}w\right)$$
23	22	riota2	$$⊢\left(C\in A\wedge \exists !z\in A\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\right)\to \left(\exists w\in BC{+}_{ℎ}D=C{+}_{ℎ}w\leftrightarrow \left(\iota z\in A|\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\right)=C\right)$$
24	17 19 23	syl2anc	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to \left(\exists w\in BC{+}_{ℎ}D=C{+}_{ℎ}w\leftrightarrow \left(\iota z\in A|\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\right)=C\right)$$
25	16 24	mpbid	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to \left(\iota z\in A|\exists w\in BC{+}_{ℎ}D=z{+}_{ℎ}w\right)=C$$
26	11 25	eqtrd	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to S\left(C{+}_{ℎ}D\right)=C$$