Theorem lcfl7lem

Description: Lemma for lcfl7N . If two functionals G and J are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015)

	Ref	Expression
Hypotheses	lcfl7lem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfl7lem.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl7lem.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl7lem.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfl7lem.a	⊢ + = ( +g ‘ 𝑈 )
	lcfl7lem.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lcfl7lem.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcfl7lem.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcfl7lem.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lcfl7lem.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfl7lem.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfl7lem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfl7lem.g	⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
	lcfl7lem.j	⊢ 𝐽 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑌 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑌 ) ) ) )
	lcfl7lem.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
	lcfl7lem.x2	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	lcfl7lem.gj	⊢ ( 𝜑 → 𝐺 = 𝐽 )
Assertion	lcfl7lem	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		lcfl7lem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfl7lem.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfl7lem.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfl7lem.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfl7lem.a	⊢ + = ( +g ‘ 𝑈 )
6		lcfl7lem.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
7		lcfl7lem.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
8		lcfl7lem.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
9		lcfl7lem.z	⊢ 0 = ( 0g ‘ 𝑈 )
10		lcfl7lem.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
11		lcfl7lem.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
12		lcfl7lem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		lcfl7lem.g	⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
14		lcfl7lem.j	⊢ 𝐽 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑌 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑌 ) ) ) )
15		lcfl7lem.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
16		lcfl7lem.x2	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
17		lcfl7lem.gj	⊢ ( 𝜑 → 𝐺 = 𝐽 )
18	1 2 3 4 9 5 6 11 7 8 13 12 15	dochsnkr2cl	⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
19	18	eldifad	⊢ ( 𝜑 → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
20	17	fveq2d	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐽 ) )
21	1 2 3 4 9 5 6 11 7 8 14 12 16	dochsnkr2	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐽 ) = ( ⊥ ‘ { 𝑌 } ) )
22	20 21	eqtrd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
23	22	fveq2d	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑌 } ) ) )
24		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
25	16	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
26	25	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
27	1 3 2 4 24 12 26	dochocsp	⊢ ( 𝜑 → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ) = ( ⊥ ‘ { 𝑌 } ) )
28	27	fveq2d	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑌 } ) ) )
29		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
30	1 3 4 24 29	dihlsprn	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
31	12 25 30	syl2anc	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
32	1 29 2	dochoc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) )
33	12 31 32	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) )
34	23 28 33	3eqtr2d	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) )
35	19 34	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) )
36	1 3 12	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
37	7 8 4 6 24	lspsnel	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ↔ ∃ 𝑠 ∈ 𝑅 𝑋 = ( 𝑠 · 𝑌 ) ) )
38	36 25 37	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑌 } ) ↔ ∃ 𝑠 ∈ 𝑅 𝑋 = ( 𝑠 · 𝑌 ) ) )
39	35 38	mpbid	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝑅 𝑋 = ( 𝑠 · 𝑌 ) )
40		simp3	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝑋 = ( 𝑠 · 𝑌 ) )
41		fveq2	⊢ ( 𝑋 = ( 𝑠 · 𝑌 ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝑠 · 𝑌 ) ) )
42	41	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝑠 · 𝑌 ) ) )
43		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
44	1 2 3 4 5 6 9 7 8 43 12 16 14	dochfl1	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑌 ) = ( 1r ‘ 𝑆 ) )
45	17	fveq1d	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 𝐽 ‘ 𝑌 ) )
46	1 2 3 4 5 6 9 7 8 43 12 15 13	dochfl1	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( 1r ‘ 𝑆 ) )
47	44 45 46	3eqtr4rd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) )
48	47	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) )
49	36	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝑈 ∈ LMod )
50	1 2 3 4 9 5 6 10 7 8 13 12 15	dochflcl	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
51	50	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝐺 ∈ 𝐹 )
52		simp2	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝑠 ∈ 𝑅 )
53	25	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝑌 ∈ 𝑉 )
54		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
55	7 8 54 4 6 10	lflmul	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑠 ∈ 𝑅 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑠 · 𝑌 ) ) = ( 𝑠 ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑌 ) ) )
56	49 51 52 53 55	syl112anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝐺 ‘ ( 𝑠 · 𝑌 ) ) = ( 𝑠 ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑌 ) ) )
57	42 48 56	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝐺 ‘ 𝑌 ) = ( 𝑠 ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑌 ) ) )
58	57	oveq1d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( ( 𝑠 ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑌 ) ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
59	7	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
60	36 59	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
61	60	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝑆 ∈ Ring )
62	7 8 4 10	lflcl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑌 ) ∈ 𝑅 )
63	36 50 25 62	syl3anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ∈ 𝑅 )
64	63	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝐺 ‘ 𝑌 ) ∈ 𝑅 )
65	1 3 12	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
66	7	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
67	65 66	syl	⊢ ( 𝜑 → 𝑆 ∈ DivRing )
68	45 44	eqtrd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 1r ‘ 𝑆 ) )
69		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
70	69 43	drngunz	⊢ ( 𝑆 ∈ DivRing → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
71	67 70	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
72	68 71	eqnetrd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ≠ ( 0g ‘ 𝑆 ) )
73		eqid	⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
74	8 69 73	drnginvrcl	⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑌 ) ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑌 ) ≠ ( 0g ‘ 𝑆 ) ) → ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝑅 )
75	67 63 72 74	syl3anc	⊢ ( 𝜑 → ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝑅 )
76	75	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝑅 )
77	8 54	ringass	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝑠 ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑌 ) ∈ 𝑅 ∧ ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝑅 ) ) → ( ( 𝑠 ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑌 ) ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( 𝑠 ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
78	61 52 64 76 77	syl13anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( ( 𝑠 ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑌 ) ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( 𝑠 ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
79	8 69 54 43 73	drnginvrr	⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑌 ) ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑌 ) ≠ ( 0g ‘ 𝑆 ) ) → ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( 1r ‘ 𝑆 ) )
80	67 63 72 79	syl3anc	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( 1r ‘ 𝑆 ) )
81	80	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( 1r ‘ 𝑆 ) )
82	81	oveq2d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝑠 ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) = ( 𝑠 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
83	58 78 82	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝑠 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( ( 𝐺 ‘ 𝑌 ) ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
84	8 54 43	ringridm	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑠 ∈ 𝑅 ) → ( 𝑠 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = 𝑠 )
85	61 52 84	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝑠 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = 𝑠 )
86	83 85 81	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝑠 = ( 1r ‘ 𝑆 ) )
87		oveq1	⊢ ( 𝑠 = ( 1r ‘ 𝑆 ) → ( 𝑠 · 𝑌 ) = ( ( 1r ‘ 𝑆 ) · 𝑌 ) )
88	4 7 6 43	lmodvs1	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ 𝑆 ) · 𝑌 ) = 𝑌 )
89	36 25 88	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) · 𝑌 ) = 𝑌 )
90	89	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( ( 1r ‘ 𝑆 ) · 𝑌 ) = 𝑌 )
91	87 90	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) ∧ 𝑠 = ( 1r ‘ 𝑆 ) ) → ( 𝑠 · 𝑌 ) = 𝑌 )
92	86 91	mpdan	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → ( 𝑠 · 𝑌 ) = 𝑌 )
93	40 92	eqtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑅 ∧ 𝑋 = ( 𝑠 · 𝑌 ) ) → 𝑋 = 𝑌 )
94	93	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝑅 𝑋 = ( 𝑠 · 𝑌 ) → 𝑋 = 𝑌 ) )
95	39 94	mpd	⊢ ( 𝜑 → 𝑋 = 𝑌 )